| Full text | |
| Author(s): |
Total Authors: 4
|
| Affiliation: | [1] Inst Aeronaut & Space, Software Engn Lab, BR-12228904 Sao Jose Dos Campos, SP - Brazil
[2] Naval Postgrad Sch, Dept Comp Sci, Monterey, CA 93943 - USA
Total Affiliations: 2
|
| Document type: | Journal article |
| Source: | IEEE SYSTEMS JOURNAL; v. 7, n. 4, p. 632-641, DEC 2013. |
| Web of Science Citations: | 3 |
| 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. (AU) | |
| FAPESP's process: | 10/08173-3 - Computer-aided validation and verification of mission critical systems |
| Grantee: | Miriam Celia Bergue Alves |
| Support Opportunities: | Scholarships abroad - Research |