Altitude Switch Controller



This example is based on the following paper published in 19th Digital Avionic Systems Conference, 7-13 October 2000, Philadelphia, PA, USA.

" Developing High Assurance Avionic Systems With the SCR Requirements Method". R. Bharadwaj and C. Heitmeyer. Naval Research Lab., Washington DC, USA.


Problem specification:

The fault-intolerant program consists of a single process that monitors a set of input sensors and issues a command to an actuator. The actuator turns on the power to a Device of Interest when the altitude of the aircraft is less than 2000 feet. The input signals are received from an analog altimeter and two digital altimeters. The system has three modes: initialization, standby, and awaitDOIon.


The input text file to our synthesis framework.

The output of our framework.