Using abstract interpretation to produce dependable aerospace control software

• Autor(es): Silva, Rovedy Aparecida Busquim e ; Arai, Nanci Naomi ; Burgareli, Luciana Akemi ; Oliveira, José M. Parente ; Pinto, Jorge Sousa
• Data: 2013
• Identificador Persistente: http://hdl.handle.net/1822/26343
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Software dependability; Formal verification; Abstract interpretation; Aerospace control software
• Tipo de Documento: Artigo
• Idioma: Inglês

Descrição

In the context of software dependability, the software veri- fication process has an important role. Formal verification of programs is an activity that can be inserted in this process to improve software reliability. This paper presents the defini- tion of an approach that employs a formal verification tech- nique based on abstract interpretation. The main goal is to apply this technique as a formal activity in the software veri- fication process to help software engineers identify programs faults. The applicability of the proposed approach is demon- strated by a case study based on embedded aerospace control software. The results obtained from its use show that abstract interpretation can contribute to software dependability.