Using Abstract Interpretation to Produce Dependable Aerospace Control Software

Citation:
Silva RAB, Arai NN, Burgareli LA, Oliveira JMP, Pinto JS.  2013.  Using Abstract Interpretation to Produce Dependable Aerospace Control Software. Industrial Track of the 6th Latin American Symposium on Dependable Computing - LADC.

Date Presented:

April

Abstract:

n the context of software dependability, the software verification 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 definition of an approach that employs a formal verification technique based on abstract interpretation. The main goal is to apply this technique as a formal activity in the software verification process to help software engineers identify programs faults. The applicability of the proposed approach is demonstrated 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.

Citation Key:

PintoJS:usiaipdacs
PreviewAttachmentSize
ladc2013109.22 KB