AADL projects having BLESS specifications, behaviors, and proofs

Examples of AADL Projects having BLESS specifications, behaviors, and correctness proofs

  • All Models Together zip file containing many AADL models with BLESS specifications, behaviors, and correctness proofs.
  • Model of Isolette example from the FAA Requirements Engineering Management Handbook (REMH).
  • VVI-mode Pacemaker single-chamber pacemaker in one thread; used as example for (NFM Paper Ref)
  • DDD-mode Pacemaker dual-chamber pacemaker with both inhibition and tracking
  • DDD with Everything dual-chamber pacemaker with all variations of pacing described in the PACEMAKER System Specification, including rate response, hysteresis, AV-squeeze, and atrial-tachycardia response
  • Open PCA Pump Kansas State University's model of a patient-controlled analgesia pump; part of the Open PCA Pump trio of design artifacts (others being requirements and assurance case) constructed under the US Food and Drug Administration's Scholar in Residence program to be a public example of high-integrity, model-based design of medical devices: Open PCA Pump Website
  • MD-VI example of medical device virtual integration for which the safety/effectiveness of composed, interoperable medical devices can be proved from formal specifications of medical devices coordinated by a BLESS control application
  • Pulse Oximeter Smart Alarmdemonstration of medical application platform (MAP) augmentation of the alarms of a pulse oximeter
  • Chinese Train Control System Created by Ehsan Ahmad including use of AADL's Hybrid Annex sublanguage to model the continuous-time differential-equation behavior of system environments
  • Adaptive Cruise Control Created in collaboration with Jean-Pierre Talpin and his team at INRIA to show the same model with behavior proved by BLESS and timing behavior analyzed by Polychrony
  • Stepper Motor Control Created in collaboration with Peter Feiler at SEI to prove correctness of a stepper-motor control of a fuel valve

  • ICE Device Project and Physical Project packages used by several of the examples above; usually included in their .zip files.
  • Eclipse needs to have the Properties -> Project References set or it can't see other projects, even if they're open in the workspace.

    Until I figure out how to create, and link a web page in Drupal

  • Proof Engine Tutorial slides describing use of the Proof Engine to annotate, and prove, correctness of a simple thread
  • Starting AADL Project for Tutorial AADL project archive containing a single thread with a BLESS annex subclause, having a state machine, and specification, but no assertions within
  • Finished AADL Project of Tutorial AADL project archive showing result of tutorial: annotated thread, proof tactic script, and proof