AADL: Pacemaker.aadl

File Pacemaker.aadl, 8.2 KB (added by pdissaux, 5 years ago)

Pacemaker AADL source code

Line 
1PACKAGE Pacemaker_Pkg
2PUBLIC
3WITH Data_Model;
4WITH Behavior_Properties;
5
6-- This simplified Pacemaker model has been developed to demonstrate the modelling
7-- capabilities of the Stood for AADL tool and the simulation features of the
8-- AADL Inspector tool.
9-- The formal specification of the behavior of the pacemaker are expressed
10-- in BLESS, whereas the "executable" implementation that is provided here
11-- uses the AADL Behavior Annex.
12-- The design documentation and the AADL source code are both automaticallly
13-- generated from the Stood model.
14
15SYSTEM Pacemaker
16END Pacemaker;
17
18-- The PACEMAKER system consists of three major components:
19-- * Device (also called the pulse generator or PG)
20-- * Device Controller-Monitor (DCM) and associated software
21-- * Leads
22SYSTEM IMPLEMENTATION Pacemaker.others
23SUBCOMPONENTS
24 PG : DEVICE PulseGenerator;
25 DCM : SYSTEM DeviceControllerMonitor.others;
26CONNECTIONS
27 cnx_0 : PORT PG.VentricleSense -> DCM.VentricleSense;
28 cnx_1 : PORT PG.AtriumSense -> DCM.AtriumSense;
29 cnx_2 : PORT DCM.VentriclePulse -> PG.VentriclePulse;
30 cnx_3 : PORT DCM.AtriumPulse -> PG.AtriumPulse;
31PROPERTIES
32 Actual_Processor_Binding => ( reference(DCM.HWPlatform) ) applies to DCM.PacemakerSW;
33END Pacemaker.others;
34
35-- The device monitors and regulates a patient's heart rate.
36-- The device detects and provides therapy for bradycardia conditions.
37-- The device provides programmable, single- and dual-chamber, rate-adaptive
38-- pacing, both permanent and temporary.
39-- In adaptive rate modes, an accelerometer is used to measure physical activity
40-- resulting in a sensor indicated rate for pacing the heart.
41-- The device is programmed and interrogated via bi-directional telemetry from
42-- the Device Controller-Monitor (DCM).
43-- This allows the physician to change the operating mode or parameters of
44-- the device non-invasively after implantation.
45
46DEVICE PulseGenerator
47FEATURES
48 VentricleSense : OUT EVENT PORT;
49 VentriclePulse : IN EVENT PORT;
50 AtriumSense : OUT EVENT PORT;
51 AtriumPulse : IN EVENT PORT;
52END PulseGenerator;
53
54-- The Device Controller-Monitor (DCM) is the primary implant, pre-discharge
55-- EP support, and follow-up device for the PACEMAKER system.
56-- The DCM is capable of being used both in the OR, physician's o±ce, and the
57-- EP lab.
58-- The DCM communicates with the PG using a communication protocol and supporting
59-- hardware.
60-- The DCM consists of the following:
61-- * A hardware platform
62-- * A pacemaker application software
63
64SYSTEM DeviceControllerMonitor
65FEATURES
66 VentricleSense : IN EVENT PORT;
67 VentriclePulse : OUT EVENT PORT;
68 AtriumSense : IN EVENT PORT;
69 AtriumPulse : OUT EVENT PORT;
70END DeviceControllerMonitor;
71
72-- The hardware platform is represented by a processor
73-- The pacemaker application software is represented by a process
74-- An Actual Processor Binding property allocates the sotware application to
75-- the processor
76SYSTEM IMPLEMENTATION DeviceControllerMonitor.others
77SUBCOMPONENTS
78 PacemakerSW : PROCESS PacemakerSW.others;
79 HWPlatform : PROCESSOR HWPlatform;
80CONNECTIONS
81 cnx_0 : PORT VentricleSense -> PacemakerSW.s;
82 cnx_1 : PORT PacemakerSW.p -> VentriclePulse;
83END DeviceControllerMonitor.others;
84
85-- The pacemaker software implements the bradycardia operating modes.
86-- In this version, only the VVI mode is supported:
87-- * the Ventricular chamber is sensed.
88-- * the Ventricular chamber is paced.
89-- * a sensnse Inhibits a pending pace.
90
91PROCESS PacemakerSW
92FEATURES
93 s : IN EVENT PORT;
94 p : OUT EVENT PORT;
95 n : OUT EVENT PORT;
96END PacemakerSW;
97
98-- The Pacemaker Software behavior can be tested as follows (in VVI mode):
99-- * Test 1) No sensing.
100-- The thread will put out an event on the "p" port every 1000 ms.
101-- * Test 2) Normal rhythm.
102-- Put an event on the "s" port every 900 ms. The thread will put an event
103-- out the "n" port each dispatch.
104-- * Test 3) Ignore sense in VRP.
105-- Wait 1000 ms for the first pace; 200 ms later put an event on the "s" port.
106-- The next pace will occur at 2000 ms.
107-- *Test 4) Pace after sense.
108-- Wait 1000 ms for the first pace; 200 ms later put an event on the "s" port,
109-- which will be ignored.
110-- At 1400 ms put out another event on the "s" port. Expect the next pace
111-- at 2400 ms.
112PROCESS IMPLEMENTATION PacemakerSW.others
113SUBCOMPONENTS
114 VRPTimeout : THREAD DualOrTimer
115 { Dispatch_Protocol => Timed;
116 Priority => 10;
117 Period => 30 ms; };
118 LRLTimeout : THREAD DualOrTimer
119 { Dispatch_Protocol => Timed;
120 Priority => 9;
121 Period => 100 ms; };
122 VVIMode : THREAD VVIMode.others;
123CONNECTIONS
124 cnx_0 : PORT s -> VVIMode.s;
125 cnx_1 : PORT VVIMode.p -> p;
126 cnx_2 : PORT VVIMode.n -> n;
127 cnx_3 : PORT VRPTimeout.output -> VVIMode.vrp_timeout;
128 cnx_4 : PORT LRLTimeout.output -> VVIMode.lrl_timeout;
129 cnx_5 : PORT VVIMode.p -> VRPTimeout.input2;
130 cnx_6 : PORT VVIMode.n -> VRPTimeout.input1;
131 cnx_7 : PORT VVIMode.p -> LRLTimeout.input2;
132 cnx_8 : PORT VVIMode.n -> LRLTimeout.input1;
133END PacemakerSW.others;
134
135-- The VRPTimeout thread sends an event 300ms after the last normal beat (n)
136-- or forced pace (p)
137-- For the purpose of the simulation, this value has been divided by 10.
138
139THREAD DualOrTimer
140FEATURES
141 input1 : IN EVENT PORT;
142 input2 : IN EVENT PORT;
143 output : OUT EVENT PORT;
144 -- The thread can be dispatched on receipt of one of its input ports or after
145 -- a fixed amount of time since the last dispatch (timeout).
146 -- The timeout delay is given by the Period property.
147 -- No explicit action is required when the thread is dispatched by an input
148 -- port (implicit action is that it sets the timer).
149 -- A send output action is performed only in the case the thread is dispatched
150 -- by the timeout event.
151ANNEX Behavior_Specification {**
152 STATES
153 s1 : INITIAL COMPLETE FINAL STATE;
154 TRANSITIONS
155 t1 : s1 -[ ON DISPATCH input1 ]-> s1;
156 t2 : s1 -[ ON DISPATCH input2 ]-> s1;
157 t3 : s1 -[ ON DISPATCH TIMEOUT ]-> s1 { output! };
158**};
159END DualOrTimer;
160
161-- The VVIMode thread reacts to sense signal and generates pulse signals.
162-- The expected behavior is:
163-- * when the heart is beating fast enough, do nothing.
164-- * when the heart has not had a beat for 1000 ms (lrl), cause a pace
165-- * if the sense comes too soon after a beat, <300 ms (vrp), ignore it.
166
167THREAD VVIMode
168FEATURES
169 s : IN EVENT PORT;
170 p : OUT EVENT PORT;
171 n : OUT EVENT PORT;
172 lrl_timeout : IN EVENT PORT;
173 vrp_timeout : IN EVENT PORT;
174END VVIMode;
175
176-- The VVIMode component can be triggered by its input event ports:
177-- * s: signals a normal heart beat that has been detected by the Pulse Generator
178-- device.
179-- * vrp_timeout: signals that the last beat occured more than 300ms ago
180-- * lrl_timeout: signals that the last beat occured more than 1000ms ago
181-- It is implemented by a thread with Aperiodic Dispatch Protocol and a Behavior
182-- Annex subclause.
183-- A data subcomponent is used to store the VRP state of the thread across
184-- the successive dispatches.
185THREAD IMPLEMENTATION VVIMode.others
186SUBCOMPONENTS
187 vrp : DATA int;
188PROPERTIES
189 Dispatch_Protocol => Aperiodic;
190 Priority => 5;
191 -- When the thread is dispatched by the vrp_timeout event, the action is to
192 -- set the vrp data subcomponent value to 0 (out of the Ventricular Refractory
193 -- Period).
194 -- When the thread is dispatched by the s (sense) event, if the vrp value
195 -- is 1 (in the Ventricular Refractory Period), ignore it; otherwise generate
196 -- a n event (normal heart beat), and set the vrp value to 1.
197 -- When the thread is dispatched by a lrl_timeout event, generate a p event
198 -- (pace) and set the vrp value to 1.
199ANNEX Behavior_Specification {**
200 STATES
201 s1 : INITIAL COMPLETE FINAL STATE;
202 TRANSITIONS
203 t0 : s1 -[ ON DISPATCH vrp_timeout ]-> s1
204 { vrp := 0 };
205 t1 : s1 -[ ON DISPATCH s ]-> s1
206 { if (vrp = 0) n!; vrp := 1 end if };
207 t2 : s1 -[ ON DISPATCH lrl_timeout ]-> s1
208 { p!; vrp := 1 };
209**};
210END VVIMode.others;
211
212-- This data subcomponent stores the Ventricular Refractory Period (VRP) state.
213-- Its value is 1 during the VRP and 0 otherwise.
214-- It is initialized to 1.
215
216DATA int
217PROPERTIES
218 Data_Model::Initial_Value => ("1");
219END int;
220
221-- The HWPlatform component represents the execution platform of the Pacemaker
222-- software.
223
224PROCESSOR HWPlatform
225PROPERTIES
226 Scheduling_Protocol => (HPF);
227END HWPlatform;
228
229END Pacemaker_Pkg;