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.


    Access

    Access via TIB

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formally specifying the logic of an automatic guidance controller


    Additional title:

    Logikspezifikation für ein avionisches Regelungssystem in ADA


    Contributors:


    Publication date :

    1991


    Size :

    12 Seiten, 1 Bild, 6 Quellen





    Type of media :

    Conference paper


    Type of material :

    Print


    Language :

    English





    Specifying Safety-Related Hazards Formally

    Troubitsyna, E. / System Safety Society | British Library Conference Proceedings | 1999


    A Learning-Based Guidance Selection Mechanism for a Formally Verified Sense and Avoid Algorithm

    Balachandran, Swee / Bajaj, Viren / Feliu, Marco A. et al. | IEEE | 2019


    A Learning-Based Guidance Selection Mechanism for a Formally Verified Sense and Avoid Algorithm

    Balachandran, Swee / Bajaj, Viren / Feliu, Marco et al. | NTRS | 2019