We describe a ectiveness of using formal methods in Space Shuttle software requirements analysis. Several Change Requests (CRs) were selected as promising targets to demonstrate the utility of formal methods in this demanding application domain. A CR to add new navigation capabilities to the Shuttle, based on Global Positioning System (GPS) technology, is the focus of this industrial usage report. Portions of the GPS CR were modeled using the language of SRI's Prototype Verication System (PVS). During a limited analysis conducted on the formal specications, numerous requirements issues were discovered. We present a summary of these encouraging results and conclusions we have drawn from the pilot project.
Formalizing New Navigation Requirements for NASA's Space Shuttle
2005
24 pages
Report
No indication
English
NASA's Space Shuttle: Perspectives on Technology Transfer
British Library Conference Proceedings | 2010
|Shuttle diplomacy [NASA's manned space flight programme]
IET Digital Library Archive | 2003
|Nasa's Management Concept for the Space Shuttle Program
Tema Archive | 1973
|