COMPSYS 705 Assignment 1 Formal Model checking and Runtime Verification

1   DDD mode pacemaker (Weighting: 15%)

Your task is to create a model of DDD mode pacemaker using UPPAAL. The created model shall be verified using UPPAAL.

1.1    Model Description

The heart model, including two components of “Random_Atrium” and “Random_Ventricle”, has been given as shown in Fig. 1.

•    Random_ Atrium:

o Inputs: AP;

o Outputs: APulse;

o Local clocks: x, x ∈  [Aminwait, Amaxwait]

o const int Amaxwait = 1200;

o const int Aminwait = 1;

•    Random_ Ventricle:

o Inputs: VP;

o Outputs: VPulse;

o Local clocks: x, x ∈  [Vminwait, Vmaxwait]

o const int Vmaxwait = 1200;

o const int Vminwait = 1;

Fig. 1. A random heart model.

A DDD mode pacemaker is capable of sensing and pacing both the atrium and ventricle. The timing constraints include [1]:

•    AEI: Atrial Escape Interval. This describes the maximum time interval between a ventricular event and the corresponding atrial event.

•    AVI: Atrial Ventricular Interval. This describes the maximum time interval between an atrial event and the corresponding ventricular event.

•    VRP: Ventricular Refractory Period. This defines the resting period for the ventricle after each

ventricular event. Physiologically, ventricular events are not detectable by the pacemaker during the resting period. That is, if VPulse, generated by the heart model, occurs within VRP, it will be   ignored by the pacemaker.

•    PVARP: Post Ventricular Atrial Refractory Period. This defines the resting period for the atrium after each ventricular event. Physiologically, atrial events are not detectable detected by the    pacemaker during the resting period. That is, if APulse, generated by the heart model, occurs   within PVARP, it will be ignored by the pacemaker.

•    URI: Upper Rate interval. This indicates the minimum time interval between two consecutive ventricular events.

•    LRI: Lower Rate Interval. This indicates the maximum time interval between two consecutive  ventricular events. In dual chamber mode, LRI time interval equals the summation of AVI and  AEI. It serves as the lower bound for the heart rate, and hence the value of LRI is greater than URI.

Fig. 2 shows examples how the DDD mode pacemaker works at some heart conditions.

Fig. 2. The timing diagram of the DDD mode pacemaker [1].

•    Waveform 1 indicates a normal heart behavior. We could observe that the related AVI timers    stop before expiry, which shows a normal synchrony between an atrial event and the following ventricular event. Likewise, the behavior of AEI shows a normal synchrony between ventricular event and the coming atrial event.

•    Waveform 2 presents the following situation where an artificial pulse (VPace) will be generated by the pacemaker if an intrinsic ventricular pulse is not sensed within the AVI interval. Also the  LRI requirement is not violated.

•    Waveform 3 features a situation where both AEI and AVI are expired. Consequently, to achieve the LRI requirement, both APace and VPace are produced.

•    Waveform 4 presents an atrial event that is earlier than usual. It may cause a temporary fast ventricular rate if there is no upper limitation. The existence of URI defers the generation of  VPace by extending the AVI interval to the length of the URI interval.

1.2    Instructions

•    Use UPPAAL to build a DDD mode pacemaker to deliver treatments conforming to the timing

constraints (const int AEI = 800; const int AVI = 150; const int VRP = 150; const int PVARP = 100; const int URI = 400; const int LRI = AEI + AVI;).

•    Perform the verification of the following properties on the closed-loop system, composed of the heart model, the DDD mode pacemaker and monitors.

1.     The system is deadlock free.

2.    A ventricular sense (VS) cannot be generated within VRP.

3.    An atrial sense (AS) cannot be generated within PVARP.

4.     The pacemaker never delivers a pacing pulse (AP) within AEI.

5.     The pacemaker never delivers a pacing pulse (VP) within AVI.

6.     The pacemaker never delivers a pacing pulse (VP) within URI.

7.     The time interval between two consecutive ventricular events is always less or equal to LRI.

8.     The pacemaker can  deliver a pacing pulse  (VP), where the  time interval between this  VP and its preceding atrial event is greater than AVI.

1.3    Marking Criteria (Weighting)

•    Modeling                                                                                     60%

o Use clocks to model the timing constraints.          60%

•    Verification                                                                                40%

o Modeling and verification of each property.         8×5%

2   References

[1]  Zhao,  Yu,  and  Partha  S.  Roop.  "Model-Driven  Design  of  Cardiac  Pacemaker  Using  IEC  61499 Function   Blocks." Distributed   Control   Applications:   Guidelines,   Design   Patterns,   and   Application Examples with the IEC 61499 9 (2016): 335.

[2] Jiang, Z., Pajic, M., Moarref, S., Alur, R., & Mangharam, R. (2012, March). Modeling and verification of a dual chamber implantable pacemaker. In International Conference on Tools and Algorithms for the

Construction and Analysis of Systems(pp. 188-203). Springer, Berlin, Heidelberg.

COMPSYS 705 Assignment 1 [Part 2]

1    Introduction

Assignment part 2 focuses on understanding and analysing a railway bridge control system using the formal policy specification tool, Easy-RV. The system is designed to manage the safe movement of trains across a shared bridge, ensuring that only one train is on the bridge at any given time.  In this assignment, the control logic is predefined, and the policies are used to verify that the system behaves according to the intended safety requirements.

2    System Overview

Figure 1: Simplified diagram of the railway bridge system.

The railway bridge connects two routes:

•  Track 1:     r1  → d1  → l1

•  Track 3:     l3  → d3

•  Track 2:     r2  → d2  → l2

•  Track 4:     l4  → d4

The system prevents two trains from occupying the bridge simultaneously by verifying mutual exclusion using signals, sensors, lights, and a switch.

3    System Variables

The system interface consists of the following boolean variables:

Inputs (Sensor variables)

•  r1, r2: Request signals from Track 1 and Track 2 respectively.

•  d1, d2, d3, d4: Sensor input detecting the presence of trains at different locations.

Outputs (Controller variables)

•  l1, l2, l3, l4: Lights that signal train access or clearance.

•  sl:  Switch signal to set the direction of the track (true = Track 1—3, false = Track 2—4).

4    Monitor states overview

The policy is named MUTEX, and it consists of several named states.  Each state defines the valid transitions and conditions for train movement or waiting.

! d1 & ! d3

d2 &  d4

r2

s 2 4 aligntracks                      s 2 4 start                        s 2 4 progress                      s 2 4 leaving

sl                  d2                     d4

1                                         1                                         1                                         1

Figure 2: Monitor states overview

This diagram is incomplete, and your task is to analyse each state’s expected safe behaviour and write the appropriate violation rules to capture the corresponding policy.

•  s wait: Idle state, waiting for any train request.

•  s   1 3 aligntracks: Preparing to allow a train from Track 1 to Track 3.

•  s   1 3 start: Track 1 train is about to start moving; switch must be correctly aligned.

•  s   1 3 progress: Track 1 train is moving over the bridge.

•  s   1 3 leaving: Track 1 train is exiting the bridge.

•  s 2 4 aligntracks: Preparing to allow a train from Track 2 to Track 4.

•  s 2 4 start: Track 2 train is about to start moving; switch must be correctly aligned.

•  s 2 4 progress: Track 2 train is moving over the bridge.

•  s 2 4 leaving: Track 2 train is exiting the bridge.

5    Tasks

For this assignment, you should extend the given template to verify the following safety policies: P1. No lights should be on while the system waits for a train request.

P2. When a train is about to start moving from Track 1, the switch (sl) must be true, and lights l2 and l4 must be off.

P3. While a train is moving from Track 1 to Track 3, the switch must remain true, and lights l1, l2, and l4 must all be off.

P4. When a train is leaving the bridge from Track 1 to Track 3, the switch must remain true, and all lights (l1—l4) must be off.

P5. When a train is about to start moving from Track 2, the switch (sl) must be false, and lights l1 and l3 must be off.

P6. While a train is moving from Track 2 to Track 4, the switch must remain false, and lights l1, l2, and l3 must all be off.

P7. When a train is leaving the bridge from Track 2 to Track 4, the switch must remain false, and all lights (l1—l4) must be off.

6    Part 2 file provided

•  RailwayBridge.erv

The Easy-RV template for this assignment. You will need to implement your policies here.

•  railwayBridge main.c

The test file in C. There are 7 test cases, one for each policy.  Compile the test file together with the auto-generated C file to test your policy.

7    Marking Scheme for Part 2 (Weighting)

8    Assignment Part 1 Submission

Please submit your answer as a single  .zip file named using the following format [YourUPI] DDDpacemaker.zip

Your .zip file must contain:

• the UPPAAL XML file for your modelling, and

• the  .q file for your verification.