Applying UML-based Formal Specification, Validation, and Verification to Space Flight Software and Defense Software
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 2011
- Accession Number
- ADA538076
Entities
People
- Doron Drusinsky
- James Bret Michael
- Konstantin Beylin
- Mantak Shing
- Miriam C. Alves
Organizations
- Naval Postgraduate School