NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Formal methods demonstration project for space applicationsThe Space Shuttle program is cooperating in a pilot project to apply formal methods to live requirements analysis activities. As one of the larger ongoing shuttle Change Requests (CR's), the Global Positioning System (GPS) CR involves a significant upgrade to the Shuttle's navigation capability. Shuttles are to be outfitted with GPS receivers and the primary avionics software will be enhanced to accept GPS-provided positions and integrate them into navigation calculations. Prior to implementing the CR, requirements analysts at Loral Space Information Systems, the Shuttle software contractor, must scrutinize the CR to identify and resolve any requirements issues. We describe an ongoing task of the Formal Methods Demonstration Project for Space Applications whose goal is to find an effective way to use formal methods in the GPS CR requirements analysis phase. This phase is currently under way and a small team from NASA Langley, ViGYAN Inc. and Loral is now engaged in this task. Background on the GPS CR is provided and an overview of the hardware/software architecture is presented. We outline the approach being taken to formalize the requirements, only a subset of which is being attempted. The approach features the use of the PVS specification language to model 'principal functions', which are major units of Shuttle software. Conventional state machine techniques form the basis of our approach. Given this background, we present interim results based on a snapshot of work in progress. Samples of requirements specifications rendered in PVS are offered to illustration. We walk through a specification sketch for the principal function known as GPS Receiver State processing. Results to date are summarized and feedback from Loral requirements analysts is highlighted. Preliminary data is shown comparing issues detected by the formal methods team versus those detected using existing requirements analysis methods. We conclude by discussing our plan to complete the remaining activities of this task.
Document ID
19960000028
Acquisition Source
Legacy CDMS
Document Type
Conference Paper
Authors
Divito, Ben L.
(Vigyan Research Associates, Inc. Hampton, VA, United States)
Date Acquired
September 6, 2013
Publication Date
June 1, 1995
Publication Information
Publication: NASA. Langley Research Center, Third NASA Langley Formal Methods Workshop
Subject Category
Computer Programming And Software
Accession Number
96N10028
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available