CS 855: Development of High-Assurance Software Systems, Spring 2021

This course will include a major project component, and this page will be updated throughout the semester to provide background material and resources for the projects.


An “Isolette” is a marketing name for an infant incubator – a medical device used to keep a new-born baby warm.

The course project will involve working with an AADL model and Slang component implementations of the Isolette. The models and implementation are based on a system description and system requirements for the Isolette given in the US Federal Aviation Administration Requirements Engineering Management Handbook (REMH). A PDF of the FAA REMH can be found here .

The project will start by working with an existing model and implementation of the Isolette. Then individual projects will be developed to address the following extentions (excerpts, others may also be considered):

  • Adding a nurses’ station monitoring system for remote monitoring of multiple infants in their Isolettes (e.g., a remote monitoring “dashboard”). This will be supported by extending HAMR to support code generation for distributed systems that communicate via JMS, DDS, or MQTT.
  • Adding features to the Operator Interface for security, by building a role-based access framework.
  • Developing a general purpose Network Interface for the Isolette (based on MQTT or DDS) to support remote monitoring and control with secure connections.
  • Adding remote logging using a Amazon Web Services connection.
  • Adding Fault Tolerance features to the Isolette including redundant sensors, etc. with a demonstration of the effectiveness of the fault-tolerant extensions based on HAMR’s fault injection framework.

Projects from Previous Semesters

PCA Pump

In a Department of Homeland Security research project, SAnToS researchers worked with Adventium Labs to develop an open source medical device platform and a Patient Controlled Analgesic Pump built using the platform. Much of the functionality of the PCA Pump has already been implemented in the Slang Embedded development framework.

This project will enhance the existing PCA Pump infrastructure by:

  • adding real-time annotations in AADL suitable for getting the project to run through the AADL schedulability analysis tools,
  • developing a deployment of the pump function on the STM 32 and Free RTOS development boards
  • developing hardware interfaces for sensors and actuators for the Open PCA Pump

The overall focus for this project is developing interfaces for realistic sensors and actuators and getting the real-time aspects of the PCA pump figured out.

Mine Water Pump Monitoring and Controlling

This is a well-known example with the formal methods and real-time systems community and is presented in detail in the book “Analyzeable Real-Time Systems: Programmed in Ada” by Alan Burns and Andy Wellings. In the book, models (but not in AADL) of the system are presented, and implementations are given in Ada.

This project will adapt the mine control implementation from the Burns and Wellings book by:

  • Re-working the modeling of the example in AADL
  • Adding real-time time annotations to AADL, following the detailed specifications in the Burns and Wellings book
  • Developing mocked-up sensors and actuators for the example to be controlled through the STM32 board (sensors: CO2, Methane, water levels, water flows; actuators: water pump, etc.)
  • Developing an operator interface for the example