The use of formal methods in software development achieves levels of quality assurance unobtainable by other means. The Larch approach to specification is described, and the specification of avionics software designed to implement the logic of a flight control system is given as an example. Penelope is described which is an Ada-verification environment. The Penelope user inputs mathematical definitions, Larch-style specifications and Ada code and performs machine-assisted proofs that the code obeys its specifications. As an example, the verification of a binary search function is considered. Emphasis is given to techniques assisting the reuse of a verification effort on modified code.


    Zugriff

    Zugriff über TIB

    Verfügbarkeit in meiner Bibliothek prüfen


    Exportieren, teilen und zitieren



    Titel :

    Formal specification and verification of Ada software


    Beteiligte:

    Kongress:

    AIAA Computing in Aerospace Conference ; 1991 ; Baltimore, MD, United States


    Erscheinungsdatum :

    01.01.1991


    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Keine Angabe


    Sprache :

    Englisch