Applying UML-based Formal Specification, Validation, and Verification to Space Flight Software and Defense Software

摘要

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.