UML-based specification, validation, and log-file based verification of the Orion Pad Abort Software
Loading...
Authors
Drusinsky, Doron
Subjects
Advisors
Date of Issue
2010-05-15
Date
Publisher
Monterey, California. Naval Postgraduate School
Language
Abstract
This paper described the first end to end application of a novel light weight formal specification, validation, and verification technique. The technique is novel is two aspects. First, it uses an intuitive, familiar, and diagrammatic notation for formal specification, a notation that being Turing equivalent and supports the capture of real-life requirements. Second, the technique includes a computer aided approach for validating the correctness of requirements early in the development process, allowing sufficient time for the correction of ambiguous and underspecified requirements. In the verification phase the technique is based on off-line verification using log-files. This approach scales well and is applicable to almost every mission critical system, including real-time systems. The paper describes the application of this technique towards the specification, validation, and verification of the Pad Abort subsystem of NASA's Orion mission.
Type
Technical Report
Description
Series/Report No
Department
Computer Science
Identifiers
NPS Report Number
NPS-CS-10-007
Sponsors
Funder
Format
23 p.: col. ill.;28 cm.
Citation
Distribution Statement
Approved for public release; distribution is unlimited.