UML-based specification, validation, and log-file based verification of the Orion Pad Abort Software
MetadataShow full item record
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.
NPS Report NumberNPS-CS-10-007
Showing items related by title, author, creator and subject.
Raque, Steven; Drusinsky, Doron (Monterey, California. Naval Postgraduate School, 2010-02-02); NPS-CS-10-002The NASA Independent Verification and Validation (IV&V) Facility is using formal specification techniques for the IV&V of the flight software for several upcoming missions. Such formal specifications are typically created ...
Michael, J.B.; Shing, M. (Monterey, California. Naval Postgraduate School, 2007-08); NPS-CS-07-008In-spite of three decades of software formal verification and validation (FV&V) research, there exists no ideal FV&V technique that works well for all FV&V concerns. That is, there is no one technique that enables (i) ...
Shi, Ronghua; Se, Xi Yang Ronald (Monterey, CA; Naval Postgraduate School, 2019-09);Verification of data-plane software is limited to verifying point properties such as bounded packet processing time or not misinterpreting malformed packet headers, which usually are chosen to illustrate the merits of some ...