End-to-end formal specification, validation and verification process: a case study of space flight software
Alves, Miriam C. Bergue
Michael, James Bret
MetadataShow full item record
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.
The article of record as published may be found at http://dx.doi.org/10.1109/JSYST.2012.2220591
Showing items related by title, author, creator and subject.
Cruickshank, Kristian John. (Monterey, California. Naval Postgraduate School, 2009-03);Validation of safety-critical software requirements is a difficult and frequently misunderstood task. It answers the question of "are we building the right product?" and is essential to Software Engineering. However, ...
UML-based specification, validation, and log-file based verification of the Orion Pad Abort Software Drusinsky, Doron (Monterey, California. Naval Postgraduate School, 2010-05-15); NPS-CS-10-007This paper described the first end to end application of a novel light weight formal specification, validation, and verification technique. The technique is novel is two aspects. First, it uses an intuitive, familiar, and ...
Applying UML-based Formal Specification, Validation, and Verification to Space Flight Control System and Defense Software Alves, Miriam C. Bergue; Beylin, Konstantin; Drusinsky, Doron; Michael, James Bret; Shing, Man-Tak (Monterey, California. Naval Postgraduate School, 2011-02-01); NPS-CS-11-003This 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 ...