Formal methods have been widely recognized as effective techniques to uncover design errors that could be missed by a conventional software engineering process. The paper describes the authors' experience with using formal methods in analyzing the redundancy management system (RMS) for a space launch vehicle. RMS is developed by AlliedSignal Inc. for the avionics of NASA's new space shuttle, called VentureStar, that meets the expectations for space missions in the 21st century. A process algebraic formalism is used to construct a formal specification based on the actual RMS design specifications. Analysis is performed using PARAGON, a toolset for formal specification and verification of distributed real-time systems. A number of real-time and fault-tolerance properties were verified, allowing some errors in the RMS pseudocode to be detected. The paper discusses the translation of the RMS specification into process algebra formal notation and results of the formal verification.
Verification of the redundancy management system for space launch vehicle: a case study
1998
10 Seiten, 16 Quellen
Aufsatz (Konferenz)
Englisch
Verification of redundancy management design
NTRS | 1978
|Design and Verification of Launch and Space Vehicle Structures
British Library Conference Proceedings | 1998
|