Applying UML-based Formal Specification, Validation, and Verification to Space Flight Control System and Defense Software
Alves, Miriam C. Bergue
Michael, James Bret
MetadataShow full item record
This report presents the process and results of a formal computer-aided Specification, Validation and Verification (SV&V) of two mission and safety critical projects: the Brazilian Satellite Launcher flight software, and the Department of Defense's Multifunctional Information Distribution System (MIDS) controller. The Specification, Validation, and Verification (SV&V) process begins with a system requirement analysis and Natural Language (NL) specification. UML statechart-formal specification assertions are then created using the StateRover SV&V specification environment; these assertions formally capture the NL requirements. The assertions are validated against the NL and cognitive requirements using JUnit-based testing within the StateRover SV&V environment. Finally, Runtime Verification (RV) is performed on the target system under test (SUT). The RV phase is based on log files created by automatically instrumenting source code files, building and executing them on the VxWorks-based target thereby creating log files, importing resulting log files into the StateRover SV&V environment and executing them as JUnit tests against the assertions.
NPS Report NumberNPS-CS-11-003
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 ...
End-to-end formal specification, validation and verification process: a case study of space flight software Alves, Miriam C. Bergue; Drusinsky, Doron; Michael, James Bret; Shing, Man-Tak (IEEE, 2013-12);The quality of requirements and the effectiveness of verification and validation (V&V) techniques in guaranteeing that a final system reflects its established requirements have a direct influence on the quality and ...
Drusinsky, Doron; Shing, Man-Tak; Demir, Kadir Alpaslan (2006);This paper addresses the need to integrate formal assertions into the modeling, implementation, and testing of statechart based designs. The paper describes an iterative process for the development and verification of ...