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.
展开▼
