A formal model for the cardiac pacemaker system is presented. Timed Coloured Petri Nets (TCPN) and CPN tools are adopted as modelling tools. The model, which includes various suitable parameters, covers numerous identified characteristics of operation modes and cardiac rhythms in substantial detail. The model can help facilitate a better understanding of the cardiac pacemaker system and provide customizable data to fully evaluate and optimize different algorithms and techniques for the pacemaker system. The obtained results prove the reliability and validity of this model in analyzing the pacemaker system while producing various cardiac events engaging the expressive power and convenience of TCPN.
of pacemaker systems. It additionally provides customizable data to assess and optimize various algorithms and parameters.
Petri Net-based models have been adopted to model some aspects of pacemakers.
In [
Moreover, other tools and techniques were applied to model the pacemaker system.
The work of [
Unlike differential equation-based models or agent-based models, this proposed TCPN-based model does not require a strong knowledge of mathematics or any programming language. The use of TCPNs, which combine graphical notations, hierarchical structures, and supported types of data sets, empowers the representation of the proposed model to be more intuitive and user-friendly as well as formally defined and analyzed.
Furthermore, in this work, not only was the pacemaker system formally verified in accordance with its specifications, the pacemaker system was also integrated into a supplementary model of the cardiac conducting systems to allow for the very detailed modelling of various cardiac rhythms and the adequate validation of the pacemaker. Finally, all processed data from this model is exportable in a customizable fashion for further analysis, optimization, and employment. 2
When a series of electrodes are placed appropriately onto the human body’s surface,
the cardiac electrical activities can then be recorded as events of signals representing
voltage over time. This recording is called the electrocardiogram (ECG) [
The ECG is the recording of cumulative signals generated by the cell population at
a given time eliciting changes in their membrane potentials. Hence, the ECG does not
directly measure the cardiac depolarization and repolarization but rather the changes in
the cardiac electrical activities over time [
The normal cardiac cycle starts with the stimulation of the senatorial node (SA),
located within the right atrium. This initial stimulation is not detected by a typical ECG as
the SA is not composed of an adequately large quantity of cells to produce a detectable
electrical potential. Instead, the depolarization of SA is conducted throughout the atria,
which can be observed as P wave in ECG. The action potentials, which next spread
throughout the atrioventricular node (VA) and the His bundle, are not large enough to
be detectable by ECG. The QRS complex indicates the depolarization result of the
ventricles. Simultaneously, atrial repolarization effects are masked by this QRS
complex due to the immense amount of tissue, thereby causing ventricular depolarization.
Thus, atrial repolarization is ordinarily undetectable in ECG. The potential of
ventricular repolarization is represented in ECG as T wave, and in some individuals, U wave
represents the late repolarization of papillary muscles. For heart anatomy and the resting
membrane potential, the reader is referred to [
Some risks associated with heart rhythms can be treated and reduced via the pacemaker system which consists of a pulse generator and one or more leads. The pulse generator (also called the device) is implanted under the skin in the pectoral area (below the collarbone), and it holds a small computer with several electronic circuits and a safely sealed battery within its case. The pulse generator functions include monitoring the heart rhythm, delivering electrical energy (i.e. pulse), and storing information about the heart. Microcomputer-based equipment (called the programmer) communicates with the pulse generator from outside the body via a wand over the skin. The programmer is used to adjust the settings of the pulse generator and retrieve the stored information. The lead is an insulated wire implanted in the heart through veins which then connects to the pulse generator. The lead transfers the heart signal to the pulse generator and returns energy from the pulse generator to the heart to maintain a healthy level of rhythms for the heart. Pacemaker devices are designed to be highly reliable. However, occasional malfunctions may prevent the delivery of therapy. Premature battery depletion, sensing or pacing issues, error codes, and/or loss of telemetry are potential malfunctions of the pacemaker system.
Coloured Petri Nets (CPNs), first proposed in [
Time in CPNs can be represented in three ways: firing duration, holding duration,
and enabling duration [
A semi-formal definition, sufficient for our purposes, can be given as follows [
CPN = (P; T; A; S ;C; N; E; G; I) where: – P is a set of places, T is a set of transitions, A is a set of arcs. – P \ T = P \ A = T \ A = 0/ – S is a set of colours. – C is a colour function that maps places in P into colours in S . – N is a node function that maps A into (P T ) [ (T P). – E is an arc expression function that maps each arc a 2 A into the expression e. The input and output types of the arc expressions must correspond to the type of nodes that the arc is connected to. – G is a guard function. It maps each transition t 2 T into guard expression g. The output of the guard expression must be evaluated as true or false. – I is an initialization function. It maps each place p into an initialization expression i. The initialization expression must evaluate a multi-set of tokens with a colour corresponding to the colour of the place C(p).
The Timed Coloured Petri Net or TCPN is defined as follows [
TCPN = (CPN; f ; M; M0) – CPN = (P; T; A; S ;C; N; E; G; I) is a Coloured Petri Net. – f : T ! [0; ¥) is a time transition function. – M : P ! [0; ¥) is a timed marking and M0 is the initial marking.
In this paper, R is used to denote real numbers and Z is used to denote integer numbers.
There are a variety of tools that can be used for CPNs (c.f. [
The pacemaker system is a hybrid embedded real-time system; its development
requirements are given and organized in [
All rate detection decisions shall be based on the measured cardiac cycle lengths of the sensed rhythm. Rate shall be evaluated on an interval-by-interval basis. – The following bradycardia operating modes shall be programmable: Off, DDDR, VDDR, DDIR, DOOR, VOOR, AOOR, VVIR, AAIR, DDD, VDD, DDI, DOO, VOO, AOO, VVI, AAI, VVT and AAT. As well, OVO, OAO, ODO, and OOO shall be available in temporary operation. (see Table 1).
Pacemaker Code The pacemaker’s operating modes are identified using a Pacemaker Code, which is a sequence of four valid letters representing four categories. Table 1 shows the four categories and their valid letters. For example, the mode AOO indicates that the pacemaker paces the atria without sensing any chamber. AAI mode indicates that the pacemaker paces and senses the atria and releases a pulse when there is no natural pulse. Groping operating codes are also possible by using the letter X as wildcard notation to denote any letter. For example, the mode AXX represents all modes that start with an A. 4
TCPN-based Modelling of Cardiac Pacemakers Different from former studies, this proposed model is composed of seven interconnected but independent submodels. Such a structure not only empowers design simplicity and flexibility but also improves observability and design coupling. These submodels include the core-elements submodel, the atrial-depolarization submodel, the AVnode submodel, the ventricular-depolarization submodel, the ST-segment submodel, the ventricular-repolarization submodel, and the artificial-pacemaker submodel. The functions and connections between these submodels are described as follows: The coreelements submodel represents the common four places among other submodels. This submodel is a part of all other submodels that exchange data across it. The atrial- depolarization submodel captures the activities of the depolarization of atrial musculature. In a healthy heart, the cardiac cycle begins with the firing of the SA node (i.e. the natural pacemaker) followed by the depolarization of atrial musculature producing the recordable P-wave in the ECG. The AV-node submodel addresses the event that follows the end of atrial depolarization. When action potentials spread through the AV node, this results in the PR segment in ECG. This is the flat line between the end of the P wave and the start of the QRS complex. The ventricular-depolarization submodel processes the right and left ventricles’ depolarization and the recordable QRS complex. The ST segment submodel addresses the time interval between the ventricular depolarization and repolarization, called the ST segment in ECG. The ventricular-repolarization submodel, as the name suggests, presents ventricular repolarization. Eventually, the artificial-pacemaker submodel monitors all the cardiac activities, ensures the implementation of pacemaker rules, and fires when specific rules, set by the programmed parameters, are met. This submodel, as shown in Figure 2, consists of four places: hPacemaker parametersi, hECG Eventsi, h Intervals and Ratiosi and hTiming Cyclei. These places also belong to other submodels. The main reason for modelling the core-elements as an independent submodel is that all other submodels contain these places of the core-element submodel. Therefore, the places are defined in an independent submodel that has a recognizable name.
The first place has the colour set Pacemaker Parameters, which is a record colour set or the Cartesian product of the sets as described in Table 2.
In the colour set Pacemaker Parameters, [modei refers to the operation mode of the artificial pacemaker as explained in Table 1. In dual-chamber modes, the hlast paced chamberi and hlast sensed chamberi are utilized to maintain the order and apply the rules accordingly. Also, hsourcei indicates the generator of a heartbeat. In a healthy heart, the Sinoatrial node (SA) is the natural pacemaker as it has the most rapid firing. Nevertheless, other cells can fire spontaneously at a slower rate as subsidiary pacemakers if the SA node permanently or temporarily ceases to fire. Consequently, hsourcei is determined based on the value of the parameter hset bpmi as defined in Table 6, and it is controlled by means of guard function on selected transitions. Similarly, hrate conditioni is based the value of parameter hset bpmi as demonstrated in Table 3.
In the colour set Pacemaker Parameters, hheartbeat counteri traces the number of generated full heartbeats. hPwave-based bpmi and hRwave-based bpmi refer to the heart rate based on the calculation of PP-interval and RR-interval. In ECG, one method to calculate the heart rate is to measure the atrial rate, indicated by PP-interval, or the ventricular rate, indicated by RR-interval. PP-interval and RR-interval represent the time between successive P waves and R waves, respectively.
The second place, as shown in Figure 2, has the colour set ECG. In principle, this is a list of generated synthetic information from ECG Event, which are defined as a record colour set or the Cartesian product of the sets described in Table 4. By default, each event, when it occurs, inserts a single element of the set ECG Event into the list of the place hECGi. However, the events of fluctuated waves insert a number of elements, with proper calculation of cumulative time, into the list of ECG based on the value of the parameters hFxi and hfxi demonstrated in Table 6. Upon generating a new event, the content of the list of ECG is dropped, and then the new event is inserted to avoid
overflow. Nevertheless, all events can be exported into text files through a monitoring tool within CPN Tools, as discussed in section simulation-based analysis.
As demonstrated in Table 4, each token of ECG Event has a unique hIDi and htitlei for the purpose of identification. The hstart timei of the event equals the hend timei of the previous event, with the exception of the initial event where the hstart timei equals the value of the parameter hinitial timei as defined in Table 6. The hend timei of the ECG event is calculated as follows:
calculated duration U (w k ; w + k ) end time = calculatedduration + start time (1) (2) – U stands for uniform distribution. – w is the value of the duration of the parameter hEvent Durationi. – k is the value of the range of the parameter hEvent Durationi.
Hence, the hcalculated durationi of an ECG event can have either a constant value in every heartbeat, or it can be assigned continuously via the uniform distribution calculation for an arbitrary value w.r.t. assigned parameters.
As ECG events are typically investigated using a number of different electrode positions or configurations, the hamplitudei of the colour set leads (defined in Table 4) denotes the estimated total height of events through the values of 12 standard ECG leads serving 12 different perspectives. The value of hamplitudei is supplied by the parameter hEvent Amplitudei. The connection of leads is presented by the parameters hBipolar Limb Leadsi, hAugmented Limb Leadsi, and hPrecordial Leadsi as defined in Table 6. If the corresponding lead parameter is set to false, then the amplitude of that lead is zero, which theoretically states an inactive lead. Otherwise, the amplitude of the lead is calculated as previously discussed.
The third presented place in Figure 2 is hinterval ratioi, and it has the colour set Interval Ratio defined in Table 5. In principle, it is a set of numerical trackers that support calculate the intervals and ratios of ECG events. The PP-interval and RR-interval are parts of the heart rate calculation previously explained in colour set Pacemaker Parameters. The event ratio is a pair:
(h; m) – h is the frequency of dropping the event (w.r.t. hEvent Durationi) – m is the total number of occurrences before the event is dropped.
The event ratio is ruled by two parameters, namely hEvent Enablementi and hEvent Ratioi as defined in Table 6. The main distinction between these two parameters is their consideration of the event’s duration time. If an event’s enablement is set to false, then it will disappear from the ECG events. However, if the event is enabled and its ratio is fulfilled, then the event is substituted by the corresponding set of hdropped eventi, which holds the event’s assigned duration with zero amplitudes. Similarly, the parameters hDropped Beat Enablementi, hDropped Beat Ratioi and hDropped Beat Durationi respectively control the occurrence, frequency, and duration for the case of dropped beats during the cardiac conduction cycle.
The hTiming Cyclei place in Figure 2 has the colour set Timing Cycle, which is a record colour set or the Cartesian product of the sets as defined in Table 7. The hIDi in the colour set Timing Cycle increases by one each time the artificial pacemaker is sensing or pacing following the defined rules (see artificial pacemaker submodel below). The hnext eventi and hlast eventi are utilized for accurate concurrent operations between the pacemaker and the heart activities if the assigned pacemaker’s operation mode declares certain engagements. As some of the pacemaker’s operation modes, such as in AOO, can pace a chamber while the heart is conducting another operation, the hevent-chunkedi, hecg-durationi and hremain-durationi in the colour set Timing Cycle control the computing of the concurrent events and, when applicable, distinguish paced events as defined in Table 4. The hpacing-ratei is calculated based on the assigned operation mode. In most modes, the hLow Rate Limit (LRL)i is the pacing rate, but in other modes where the hRate modulationi (i.e. XXXR) is set, the hMaximum Sensor Rate (MSR)i is considered during calculation. The values of hcurrent-pacing-occurrenci and hnext-pacing-durationi are continuously computed with every new cycle based on the programmed parameters. Finally, the colour set of htimersi represents the computed values of the assigned parameters explained in Table 6.
operation mode
LRL
URL
AV Delay
Dynamic AV Delay Sensed AV Delay Offset A amplitude V amplitude
A width V width VRP ARP
PVARP PVARP Extension
ATR mode ATR duration ATR Fallback
MSR Activity Threshold Response Factor Reaction Time Recovery Time Rate Smoothing
initial time number of beats
set bpm Event Enablement
Event Duration
or fx) Event Amplitude
Event Ratio Dropped Beat
Enablement Dropped Beat Ratio Dropped Beat Duration Connections of Leads
Off DDD VDD DDI DOO AOO AAI VOO VVI AAT VVT DDDR
VDDR DDIR DOOR AOOR
AAIR VOOR VVIR f(ARP [ VRP [ LRL [ URL [ MSR [ ATR [ AV-delay [ V-blanking [ A-blanking [ PVARP [ VA-interval) j timers 2 R g f(ID, next event, last event, event-chunked, pacing-rate, ecg-duration, remain-duration, timetracker, current-pacing-occurrenc, next-pacing-duration, timers ) j ID, event-chunked 2 Z>1 next event, last event 2 event, pacing-rate, ecg-duration, remain-duration, time-tracker, current-pacingoccurrenc, next-pacing-duration 2 R>0, timers 2 timersg As shown in Figure 3, this submodel demonstrates the recorded ECG event, P-wave, during the atrial depolarization. The processing of P-wave, if enabled, is determined based on the computing of the tokens from all the four connected places explained in the previous submodel. The token of place hTiming Cyclei has the timestamps of a real number, which initially equals the value of the parameter hinitial timei, and after that equals the continuous cumulative timestamps of the model. The firing of transition hstimulate atriali is only enabled if its guard, which represents appropriate rules, is holding. The specific rules that must be satisfied are as follows: – The value of hnext eventi from the colour set Timing Cycle, defined in Table 7, equals P-wave, dropped-Pwave, or paced-Pwave. – If the value of the parameter hnumber of beatsi is greater than zero, then the number of modelled full heartbeats must be less than or equal to the value of this parameter. – If the value of the parameter hnumber of beatsi equals zero, then the number of modelled full heartbeats is not restricted.
[stop_simulation(gs) andalso grant_privilege(gt,P_wave)]
TCIV Ttimingt1_Ccycle
Iintervai1l_Rratio IRIV stimulate atrial { input (ge,gi,gt,gs);output (se,si,d,st,ss); }
action(upd(ge,gi,gt,gs));
gt se ge gi gs si ss
ECGEeCE1Gvent
Ppacemaker_pp1arameters PMIV
After firing transition hstimulate atriali, all tokens are computed according to the event’s parameters, and they are returned to their original places. Like the previous submodel, the AV-Node submodel (Figure 4) represents the ECG event’s PR segment. The transition hpresent PR segmenti is enabled if and only if the value of hnext eventi from the colour set Timing Cycle equals PR-segment, droppedPRsegment, or paced-PRsegment. Upon the firing of transition hpresent PR segmenti, all tokens from all connected places are concurrently calculated by their defined parameters and then returned to their original places.
[grant_privilege(gt,PR_segment)]
TCIV Ttimingt2_Ccycle
Iintervai2l_Rratio IRIV gt gi
si present PR segment { iancptiuotn((guep,dg(ig,get,,ggis,g);to,gust)p)u;t (se,si,d,st,ss); } se ge gs
ss
ECGEeCE2vGent
Ppacemaker_pp2arameters PMIV The Ventricular-Depolarization submodel, as shown in Figure 5, discusses the QRS complex, which expresses the ventricular depolarization. This submodel is composed of three transitions interpreting the waves of the QRS complex. Each transition is enabled and fired when its guard is fulfilled according to the value of hnext eventi from the colour set Pacemaker Parameters. Consequently, the tokens of connected places are appropriately updated. In Figure 6, the ST-segment submodel, as the name suggests, denotes the ST segment of the ECG event. When transition hpresent ST segmenti is fired, tokens are computed as in previous submodels. This submodel demonstrates the repolarization of ventricular through the ECG events; T-wave, TU-segment, U-wave, and TP-segment. As the tokens are computed via firing fulfilled transitions, those tokens of associated places are modernized thoroughly concerning the related parameters’ values as discussed in the core-elements submodel. TCIV
Ttimingt4_Ccycle
Iinterv ai4l_Rratio
IRIV gt ge se
ge stimulate major ventricular {
gt stimulate basal { gt ge se gi gs gs gi gi gs si ss ss si si ss
ECGEeCE4Gvent
Ppacemaker_pp4arameters
PMIV TCIV
Ttimintg4_2Ccycle
Iintervia4l2_Rratio
IRIV [grant_privilege(gt,Q_wave)] stimulate septal {
ECGEeC4EGv2ent
Ppacemakerp_4p2arameters
PMIV gt gi
si present ST segment {
ECGEeCE5vGent
Ppacemaker_pp5arameters
PMIV gi gs gs gi gi gs gi si ss si si ss si [grant_privilege(gt,TU_segment)] [grant_privilege(gt,U_wave)] [grant_privilege(gt,TP_segment)] present TU segment { iancptiuotn((guep,dg(ig,get,,ggis,g);to,gust)p)u;t (se,si,d,st,ss); } TCIV Ttimintg6_2Ccycle
Iintervia6l2_Rratio IRIV repolarize papillary muscles { iancptiuotn((guep,dg(ig,get,,ggis,g);to,gust)p)u;t (se,si,d,st,ss); } se ge gs
ss 1`[] ECGEeC6EGv2ent
Ppacemakerp_6p2arameters PMIV full heartbeat { iancptiuotn((guep,dg(ig,get,,ggis,g);to,gust)p)u;t (se,si,d,st,ss); }
[grant_privilege(gt,T_wave)] TCIV Ttimingt6_Ccycle
Iintervai6l_Rratio IRIV repolarize ventrical { iancptiuotn((guep,dg(ig,get,,ggis,g);to,gust)p)u;t (se,si,d,st,ss); }
ss This last submodel (Figure 8) signifies the artificial pacemaker’s functions and operations. The firing of transition hartificial pacingi is only enabled if its guard, which considers relevant rules, is holding. The specific rules that must be satisfied are as follows: – The value of parameter hoperation modei (Table 6) indicates chamber pacing as in
AXXX, VXXX, and DXXX (Table 1). – The value of hnext eventi from the colour set Timing Cycle, defined in Table 7, equals hartifical-pacingi. – The current time of the model equals the calculation of hpacing ratei (Table 7) – The associated htimersi of the applied hoperation modei equal their assigned values.
After firing transition hartificial pacingi, tokens are computed accordingly, and then associated places are updated with the processed tokens.
[grant_privilege(gt,artificial_pacing)]
TCIV Ttimingt7_Ccycle 0 gt gi
si artificial pacing { input (ge,gt,gs,gi);output (se,st,ss,d,si); }
action(pm(ge,gt,gs,gi)); se ge gs
ss 1`[] ECGEeCE7vGent
Ppacemaker_pp7arameters PMIV
The analysis is conducted utilizing a test scenario methodology. All the required
operation modes, declared by the requirements, were exhaustively verified in accordance
with their associated parameters. These operation modes were also validated with
various cardiac rhythms where assumed results were sustainably met. For instance, one
of the analyzed test scenarios is a natural pacemaker (i.e. the heart) that failed with
combined sinus node dysfunction and AV node dysfunction. Usually, a dual-chamber
pacemaker with operation mode DDD or DDDR is chosen. Subsequently, the values
of the associated parameter of the selected operation mode were configured
following the system specifications [
Various techniques and tools can be applied to analyze CPN-based models [
The significant results of the simulation-based analysis include the following: – A more solid understanding of and reliance upon the correctness of the model’s design was gained. Simulation modelling assists in recognizing and debugging errors in the model’s constructions and definitions. – The comprehensiveness of the model’s specification was assured. This is important as incomplete specifications prohibit the model’s desired execution. – Design flaws were corrected and particular sequences were examined to reflect the system’s behaviour in selected scenarios. – The simulations show that the model appears to terminate in the desired consistent state under its parameters correctly. – In addition, user-defined monitors were applied to selectively export generated tokens of the ECG events into text-based files. Such exported data can then be utilized to adequately evaluate and optimize different algorithms and techniques. Nevertheless, the simulation-based technique cannot guarantee that all possible executions are covered; therefore, State Space analysis is conducted to verify other functional and performance properties. 5.2
State Space Analysis State Space analysis is a formal verification technique typically performed by a computer tool to construct a directed graph of arcs and nodes. The nodes represent reachable markings (the model’s states), and the arcs represent enabled binding elements (state transformations). As enabled binding elements are executed until all reachable markings are generated, thereby giving all possible model states, various properties of the model can then be verified. The behavioural properties reported by the Space State analysis include some statistical information, boundedness properties, and other properties.
The strongly-connected-component graph (SCC graph) is often derived from the State Space’s graph structure. CPN State Space tool uses the SCC graph to assess the standard behavioural properties of the model. Nevertheless, the calculation of timed state space can be complicated and laborious in part because the size of the reachability graph can be infinite as several timed markings with global clock and timestamps are distinguished. In such a case, the model can be analyzed for a defined period of time to limit the infinite markings due to the global clock.
In this paper, four scenarios are analyzed. Each scenario has a specific operation mode and parameters set to the norm values. These selected operation modes are OAO, DOO, VDD, and DDDR, with a total of 1000, 2000, 3000, and 6500 heartbeats, respectively.
For all operation modes, the reported statistical results hold similar features. As shown in Table 8, the numbers of nodes and arcs in the SCC graph are always identical to State Space’s corresponding numbers. As expected, this implies that the model has no cyclical behaviour. Even though the numbers of nodes and arcs are equal for both State Space and SCC graph in this proposed model, these numbers may not always agree based on the model’s specifications. When the number of SCC-graph nodes is fewer than the number of State-Space nodes, this indicates that there are non-trivial SCCs and cycles in the State Space of the model (i.e. may not terminate).
The reachability properties’ results indicate that an occurrence sequence exists in a sequential direction. By performing standard query functions, it was observed that the occurrence sequence, in all scenarios, returns true only between nodes in ascending order. This behaviour is anticipated since the model is time-based. The boundedness properties report the number of tokens for places after executing all reachable markings. In all scenarios, the quantity of one token was reported as the maximal and minimal number of tokens that can remain, in any reachable marking, on each place. Similar to reachability properties’ results, the boundedness properties’ results matched the assumed numbers in accordance with the timed characteristics of this model. The home properties’ results, by design, indicate no home marking that is reachable from any other marking.
The liveness properties’ results address dead markings, dead transition instances, and live transition instances. Dead markings are those with unenabled binding elements which result from nodes holding tokens with no outgoing arcs or disabled transitions. For all scenarios, a single dead marking was reported. This is typically expected with models that should terminate at a certain point by design. The results of dead transition instances indicate the transitions that were never enabled (i.e. fired) during the model’s execution. When the results of dead transition instances are reported as None, this implies that all the transitions in the model have the opportunity of firing (occurring) at least once. According to the adopted operation modes and parameters, two scenarios hold no dead transition instances. In comparison, each of the other two scenarios register a single dead transition instance. This result is interpreted as indicating that the pacemaker did not deliver any electrical impulses following the designated parameters. On the other hand, the results of live transition instances state the transitions that are reachable in the occurrence sequence of any reachable marking. All four scenarios contain no live transition instances, thereby determining that each transition is not always found in the occurrence sequence of any reachable marking. Models with dead markings regularly have no live transition instances because the model was terminated. Dead transitions are not the opposite of live transitions since a non-dead transition must be enabled at least once while a live transition should continue to be enabled. Finally, the fairness properties’ results represent a list of all impartial transitions which occur infinitely. When such transitions are removed or restricted, all infinite occurrence sequences of the model will be subsequently eliminated if desired. As expected in accordance with the parameters and specifications, there are no infinite occurrence sequences in any scenario. 6
Software verification is an ongoing challenge. More studies and efforts in this area will eventually assist in the development of more reliable software. As a pilot problem for the Verified Software Initiative, modelling the pacemaker system through different formalisms will not only lead to a more concrete understanding of current tools but will also drive more comprehensive comparison among them. This paper demonstrates the expressive power and reliability of TCPNs towards modelling safety-critical systems such as the pacemaker system. Nevertheless, the number of CPN-based models concerning the verification of the pacemaker system is limited and insufficient.
Consequently, this study aimed to contribute to the verification and validation of the pacemaker system and to present a practical methodology when approaching similar systems. The model is formed of seven submodels to augment its legibility and adaptability. In addition, the model can assist not only in facilitating a better understanding of pacemakers and relevant cardiac events but also in producing customizable data to judge and optimize different relevant algorithms and techniques sufficiently.