NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal specification and verification of Ada softwareThe 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.
Document ID
19920034961
Acquisition Source
Legacy CDMS
Document Type
Conference Paper
Authors
Hird, Geoffrey R.
(Ora Corp. Ithaca, NY, United States)
Date Acquired
August 15, 2013
Publication Date
January 1, 1991
Subject Category
Computer Programming And Software
Report/Patent Number
AIAA PAPER 91-3713
Meeting Information
Meeting: AIAA Computing in Aerospace Conference
Location: Baltimore, MD
Country: United States
Start Date: October 21, 1991
End Date: October 24, 1991
Accession Number
92A17585
Funding Number(s)
CONTRACT_GRANT: NAS1-18972
Distribution Limits
Public
Copyright
Other

Available Downloads

There are no available downloads for this record.
No Preview Available