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.
Formal specification and verification of Ada software
AIAA Computing in Aerospace Conference ; 1991 ; Baltimore, MD, United States
01.01.1991
Aufsatz (Konferenz)
Keine Angabe
Englisch
Formal specification and verification of Ada software
AIAA | 1991
|Formal Specification of Software Critical Systems with Agents
British Library Conference Proceedings | 1995
|Formal Verification of Flight Critical Software
AIAA | 2005
|