Publication Date:
2019-07-13
Description:
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.
Keywords:
COMPUTER PROGRAMMING AND SOFTWARE
Type:
AIAA PAPER 91-3713
,
AIAA Computing in Aerospace Conference; Oct 21, 1991 - Oct 24, 1991; Baltimore, MD; United States
Format:
text
Permalink