The Transportation Systems Research Vehicle (TSRV) is a specially equipped Boeing 737 operated by NASA's Langley Research Center as part of the Advanced Transport Operating Systems program. It is used as a laboratory to study the development, implementation, and certification of digital flight control systems. The logic of the interface through which the pilot communicats with the flight control software of the TSRV is quite complex, and is difficult to describe clearly by ad hoc means. This paper describes work-in-progress, the development of a formal specification of an Ada implementation using the Larch/Ada specification language, the language of the Penelope verification system.
Formally specifying the logic of an automatic guidance controller
Logikspezifikation für ein avionisches Regelungssystem in ADA
1991
12 Seiten, 1 Bild, 6 Quellen
Conference paper
English
Specifying Safety-Related Hazards Formally
British Library Conference Proceedings | 1999
|