Using abstract interpretation to produce dependable aerospace control software

• Author(s): Silva, Rovedy Aparecida Busquim e ; Arai, Nanci Naomi ; Burgareli, Luciana Akemi ; Oliveira, José M. Parente ; Pinto, Jorge Sousa
• Date: 2013
• Persistent ID: http://hdl.handle.net/1822/26343
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Software dependability; Formal verification; Abstract interpretation; Aerospace control software
• Document Type: Article
• Language: English

Description

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.