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.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formally specifying the logic of an automatic guidance controller


    Weitere Titelangaben:

    Logikspezifikation für ein avionisches Regelungssystem in ADA


    Beteiligte:
    Guaspari, D. (Autor:in)


    Erscheinungsdatum :

    1991


    Format / Umfang :

    12 Seiten, 1 Bild, 6 Quellen





    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Print


    Sprache :

    Englisch





    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