AADL: Pacemaker.aadl

PACKAGE Pacemaker_Pkg
PUBLIC
WITH Data_Model;
WITH Behavior_Properties;

-- This simplified Pacemaker model has been developed to demonstrate the modelling
--  capabilities of the Stood for AADL tool and the simulation features of the
--  AADL Inspector tool. 
-- The formal specification of the behavior of the pacemaker are expressed
--  in BLESS, whereas the "executable" implementation that is provided here
--  uses the AADL Behavior Annex.
-- The design documentation and the AADL source code are both automaticallly
--  generated from the Stood model.

SYSTEM Pacemaker
END Pacemaker;

-- The PACEMAKER system consists of three major components:
-- * Device (also called the pulse generator or PG)
-- * Device Controller-Monitor (DCM) and associated software
-- * Leads
SYSTEM IMPLEMENTATION Pacemaker.others
SUBCOMPONENTS
  PG : DEVICE PulseGenerator;
  DCM : SYSTEM DeviceControllerMonitor.others;
CONNECTIONS
  cnx_0 : PORT PG.VentricleSense -> DCM.VentricleSense;
  cnx_1 : PORT PG.AtriumSense -> DCM.AtriumSense;
  cnx_2 : PORT DCM.VentriclePulse -> PG.VentriclePulse;
  cnx_3 : PORT DCM.AtriumPulse -> PG.AtriumPulse;
PROPERTIES
  Actual_Processor_Binding => ( reference(DCM.HWPlatform) ) applies to DCM.PacemakerSW;
END Pacemaker.others;

-- The device monitors and regulates a patient's heart rate.
-- The device detects and provides therapy for bradycardia conditions.
-- The device provides programmable, single- and dual-chamber, rate-adaptive
--  pacing, both permanent and temporary.
-- In adaptive rate modes, an accelerometer is used to measure physical activity
--  resulting in a sensor indicated rate for pacing the heart.
-- The device is programmed and interrogated via bi-directional telemetry from
--  the Device Controller-Monitor (DCM). 
-- This allows the physician to change the operating mode or parameters of
--  the device non-invasively after implantation.

DEVICE PulseGenerator
FEATURES
  VentricleSense : OUT EVENT PORT;
  VentriclePulse : IN EVENT PORT;
  AtriumSense : OUT EVENT PORT;
  AtriumPulse : IN EVENT PORT;
END PulseGenerator;

-- The Device Controller-Monitor (DCM) is the primary implant, pre-discharge
--  EP support, and follow-up device for the PACEMAKER system. 
-- The DCM is capable of being used both in the OR, physician's o±ce, and the
--  EP lab.
-- The DCM communicates with the PG using a communication protocol and supporting
--  hardware. 
-- The DCM consists of the following:
-- * A hardware platform
-- * A pacemaker application software

SYSTEM DeviceControllerMonitor
FEATURES
  VentricleSense : IN EVENT PORT;
  VentriclePulse : OUT EVENT PORT;
  AtriumSense : IN EVENT PORT;
  AtriumPulse : OUT EVENT PORT;
END DeviceControllerMonitor;

-- The hardware platform is represented by a processor
-- The pacemaker application software is represented by a process
-- An Actual Processor Binding property allocates the sotware application to
--  the processor
SYSTEM IMPLEMENTATION DeviceControllerMonitor.others
SUBCOMPONENTS
  PacemakerSW : PROCESS PacemakerSW.others;
  HWPlatform : PROCESSOR HWPlatform;
CONNECTIONS
  cnx_0 : PORT VentricleSense -> PacemakerSW.s;
  cnx_1 : PORT PacemakerSW.p -> VentriclePulse;
END DeviceControllerMonitor.others;

-- The pacemaker software implements the bradycardia operating modes.
-- In this version, only the VVI mode is supported:
-- * the Ventricular chamber is sensed.
-- * the Ventricular chamber is paced.
-- * a sensnse Inhibits a pending pace.

PROCESS PacemakerSW
FEATURES
  s : IN EVENT PORT;
  p : OUT EVENT PORT;
  n : OUT EVENT PORT;
END PacemakerSW;

-- The Pacemaker Software behavior can be tested as follows (in VVI mode):
-- * Test 1)  No sensing.
-- The thread will put out an event on the "p" port every 1000 ms.
-- * Test 2)  Normal rhythm.
-- Put an event on the "s" port every 900 ms.  The thread will put an event
--  out the "n" port each dispatch.
-- * Test 3)  Ignore sense in VRP.
-- Wait 1000 ms for the first pace; 200 ms later put an event on the "s" port.
--   The next pace will occur at 2000 ms.
-- *Test 4)  Pace after sense.
-- Wait 1000 ms for the first pace; 200 ms later put an event on the "s" port,
--  which will be ignored.
-- At 1400 ms put out another event on the "s" port.  Expect the next pace
--  at 2400 ms.
PROCESS IMPLEMENTATION PacemakerSW.others
SUBCOMPONENTS
  VRPTimeout : THREAD DualOrTimer
    { Dispatch_Protocol => Timed;
      Priority => 10;
      Period => 30 ms; };
  LRLTimeout : THREAD DualOrTimer
    { Dispatch_Protocol => Timed;
      Priority => 9;
      Period => 100 ms; };
  VVIMode : THREAD VVIMode.others;
CONNECTIONS
  cnx_0 : PORT s -> VVIMode.s;
  cnx_1 : PORT VVIMode.p -> p;
  cnx_2 : PORT VVIMode.n -> n;
  cnx_3 : PORT VRPTimeout.output -> VVIMode.vrp_timeout;
  cnx_4 : PORT LRLTimeout.output -> VVIMode.lrl_timeout;
  cnx_5 : PORT VVIMode.p -> VRPTimeout.input2;
  cnx_6 : PORT VVIMode.n -> VRPTimeout.input1;
  cnx_7 : PORT VVIMode.p -> LRLTimeout.input2;
  cnx_8 : PORT VVIMode.n -> LRLTimeout.input1;
END PacemakerSW.others;

-- The VRPTimeout thread sends an event 300ms after the last normal beat (n)
--  or forced pace (p)
-- For the purpose of the simulation, this value has been divided by 10.

THREAD DualOrTimer
FEATURES
  input1 : IN EVENT PORT;
  input2 : IN EVENT PORT;
  output : OUT EVENT PORT;
  -- The thread can be dispatched on receipt of one of its input ports or after
  --  a fixed amount of time since the last dispatch (timeout).
  -- The timeout delay is given by the Period property.
  -- No explicit action is required when the thread is dispatched by an input
  --  port (implicit action is that it sets the timer).
  -- A send output action is performed only in the case the thread is dispatched
  --  by the timeout event.
ANNEX Behavior_Specification {**
  STATES 
    s1 : INITIAL COMPLETE FINAL STATE;
  TRANSITIONS
    t1 : s1 -[ ON DISPATCH input1 ]-> s1;
    t2 : s1 -[ ON DISPATCH input2 ]-> s1;
    t3 : s1 -[ ON DISPATCH TIMEOUT ]-> s1 { output! };
**};
END DualOrTimer;

-- The VVIMode thread reacts to sense signal and generates pulse signals.
-- The expected behavior is:
-- * when the heart is beating fast enough, do nothing.
-- * when the heart has not had a beat for 1000 ms (lrl), cause a pace
-- * if the sense comes too soon after a beat, <300 ms (vrp), ignore it.

THREAD VVIMode
FEATURES
  s : IN EVENT PORT;
  p : OUT EVENT PORT;
  n : OUT EVENT PORT;
  lrl_timeout : IN EVENT PORT;
  vrp_timeout : IN EVENT PORT;
END VVIMode;

-- The VVIMode component can be triggered by its input event ports:
-- * s: signals a normal heart beat that has been detected by the Pulse Generator
--  device.
-- * vrp_timeout: signals that the last beat occured more than 300ms ago
-- * lrl_timeout: signals that the last beat occured more than 1000ms ago
-- It is implemented by a thread with Aperiodic Dispatch Protocol and a Behavior
--  Annex subclause.
-- A data subcomponent is used to store the VRP state of the thread across
--  the successive dispatches.
THREAD IMPLEMENTATION VVIMode.others
SUBCOMPONENTS
  vrp : DATA int;
PROPERTIES
  Dispatch_Protocol => Aperiodic;
  Priority => 5;
  -- When the thread is dispatched by the vrp_timeout event, the action is to
  --  set the vrp data subcomponent value to 0 (out of the Ventricular Refractory
  --  Period).
  -- When the thread is dispatched by the s (sense) event, if the vrp value
  --  is 1 (in the Ventricular Refractory Period), ignore it; otherwise generate
  --  a n event (normal heart beat), and set the vrp value to 1.
  -- When the thread is dispatched by a lrl_timeout event, generate a p event
  --  (pace) and set the vrp value to 1.
ANNEX Behavior_Specification {**
  STATES 
    s1 : INITIAL COMPLETE FINAL STATE;
  TRANSITIONS
    t0 : s1 -[ ON DISPATCH vrp_timeout ]-> s1
      { vrp := 0 };
    t1 : s1 -[ ON DISPATCH s ]-> s1 
      { if (vrp = 0) n!; vrp := 1 end if };
    t2 : s1 -[ ON DISPATCH lrl_timeout ]-> s1 
      { p!; vrp := 1 };
**};
END VVIMode.others;

-- This data subcomponent stores the Ventricular Refractory Period (VRP) state.
-- Its value is 1 during the VRP and 0 otherwise.
-- It is initialized to 1.

DATA int
PROPERTIES
  Data_Model::Initial_Value => ("1");
END int;

-- The HWPlatform component represents the execution platform of the Pacemaker
--  software.

PROCESSOR HWPlatform
PROPERTIES
  Scheduling_Protocol => (HPF);
END HWPlatform;

END Pacemaker_Pkg;