Applying UML-based Formal Specification, Validation, and Verification to Space Flight Software and Defense Software
Miriam C. Bergue Alves, Konstantin Beylin, Doron Drusinsky, James Michael, Man‐Tak Shing · 2011
Abstract : This report presents the process and results of a formal computer-aided Specification, Validation and Verification (SVV 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.