End-to-End Formal Specification, Validation, and Verification Process: A Case Study of Space Flight Software

Autor(es)

Bergue Alves, Miriam C. ^[1] ; Drusinsky, Doron ^[2] ; Michael, James Bret ^[2] ; Shing, Man-Tak ^[2]

Afiliação do(s) autor(es)

^[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

• Tipo de documento: Artigo Científico
• Fonte: IEEE SYSTEMS JOURNAL; v. 7, n. 4, p. 632-641, DEC 2013.
• Citações Web of Science: 3

Resumo

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)

• Processo FAPESP: 10/08173-3 - Verificação e validação de sistemas de missão crítica
• Beneficiário: Miriam Celia Bergue Alves
• Modalidade de apoio: Bolsas no Exterior - Pesquisa