NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
An introduction to requirements capture using PVS: Specification of a simple autopilotThis paper presents an introduction to capturing software requirements in the PVS formal language. The object of study is a simplified digital autopilot that was motivated in part by the mode control panel of NASA Langley's Boeing 737 research aircraft. The paper first presents the requirements for this autopilot in English and then steps the reader through a translation of these requirements into formal mathematics. Along the way deficiencies in the English specification are noted and repaired. Once completed, the formal PVS requirement is analyzed using the PVS theorem prover and shown to maintain an invariant over its state space.
Document ID
19960042551
Acquisition Source
Langley Research Center
Document Type
Technical Memorandum (TM)
Authors
Butler, Ricky W. (NASA Langley Research Center Hampton, VA United States)
Date Acquired
September 6, 2013
Publication Date
May 1, 1996
Subject Category
Computer Programming And Software
Report/Patent Number
NASA-TM-110255
NAS 1.15:110255
Report Number: NASA-TM-110255
Report Number: NAS 1.15:110255
Accession Number
96N31527
Funding Number(s)
PROJECT: RTOP 505-64-10-13
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available