End-to-end formal specification, validation and verification process: a case study of space flight software
Loading...
Authors
Alves, Miriam C. Bergue
Drusinsky, Doron
Michael, James Bret
Shing, Man-Tak
Subjects
Astronautics
Behavior
Formal methods
Metrics
Process
Requirements engineering
Runtime execution monitoring
Software
Statechart assertions
Verification and validation (V&V)
Behavior
Formal methods
Metrics
Process
Requirements engineering
Runtime execution monitoring
Software
Statechart assertions
Verification and validation (V&V)
Advisors
Date of Issue
2013-12
Date
Publisher
IEEE
Language
Abstract
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 dependability of the delivered system. The V&V process can be efficient from a managerial point of view, but ineffective from a technical perspective, and vice versa. This paper presents an end-to-end formal computer-aided specification, validation, and verification (SV&V) process, whose feasibility and effectiveness were evaluated against the flight software for the Brazilian Satellite Launcher. Unified modeling language (UML) statechart assertions, scenario-based validation, and runtime verification are used to formally specify and verify the system, and metrics of the ongoing process and its V&V results are collected during the application of the process. The results of the case study indicate that the process and its computer-aided environment were both technically feasible to apply and managerially effective, will likely scale well to cater to SV&V of mission-critical systems that have a larger number of behavioral requirements, and can be used for V&V in a distributed development environment.
Type
Article
Description
The article of record as published may be found at http://dx.doi.org/10.1109/JSYST.2012.2220591
Series/Report No
Department
Computer Science (CS)
Organization
Naval Postgraduate School (U.S.)
Identifiers
NPS Report Number
Sponsors
Funder
Format
10 p.
Citation
M.C.B. Alves, D. Drusinsky, J.B. Michael, M.-T. Shing, "End-to-end formal specification, validation and verification process: a case study of space flight software," IEEE Systems Journal, v.7, no.4, (December 2013), pp. 632-641.
Distribution Statement
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.