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
Eclipse needs to have the Properties -> Project References set or it can't see other projects, even if they're open in the workspace.