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.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Formal specification and verification of Ada software


    Contributors:

    Conference:

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


    Publication date :

    1991-01-01


    Type of media :

    Conference paper


    Type of material :

    No indication


    Language :

    English