This page links to AADL models with BLESS 2 behaviors and specifications. BLESS 3 examples can be found here.

The first BLESS program was for an AADL thread controlling cardiac pacemaker behavior in “VVI” mode. The first V indicates pacing in the (right) ventricle; the second V indicates sensing in the (right) ventricle, and the I indicates that sensing of normal cardiac behavior inhibits pacing. This paper discussed VVI .

The second BLESS program performed “DDD” mode cardiac pacing. The first D indicates dual pacing in both the right atrium and right ventricle. The second D indicates dual sensing in both chambers. The third D indicates dual behavior–both inhibition and tracking. Tracking will pace the ventricle after contraction is sensed in the atrium if ventricular contraction is not detected within a prescribed time. DDD was vastly more complex than VVI.

Boston Scientific released the PACEMAKER System Specification, from which the behaviors for VVI and DDD were taken. PACEMAKER has many more options including rate response (pacing faster when an accelerometer detects motion), hysteresis, rate smoothing, and atrial tachycardia response among others. DDDwE (with everything) supports all therapy features in any combination so long as the prescription parameters don’t conflict. (For actual devices, a programmer that communicates with a pacemaker enforces rules regarding the relationships of prescription parameters.) See Formal semantics for the PACEMAKER System Specification.

Pulse Oximeter Smart Alarm

Stepper Motor Controller

Chinese Train Control System

Building Control

ICE Device

Physical Properties and Types

Isolette

Medical Device Virtual Integration (MD-VI)

Water-Level Control System