An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot
Ricky W. Butler · NASA Technical Reports Server (NASA) · 1996
This 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. KEYWORDS: Formal Methods, Software Requirements, Verification, Autopilot 1 Introduction In this paper, the process of translating requirements into a formal language will be explored. The chosen target specification language is SRI International's PVS Language[10], however, the modeling techniques used in this paper can be used with other formal specif...