Formal Verification With Frama-C: A Case Study in the Space Software Domain

Thumbnail Image
Date
2016
Authors
Busquim e Silva,RABE
Arai,NN
Burgareli,LA
Parente de Oliveira,JMP
Jorge Sousa Pinto
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
With the increasing importance of software in the aerospace field, as evidenced by its growing size and complexity, a rigorous and reliable software verification and validation process must be applied to ensure conformance with the strict requirements of this software. Although important, traditional validation activities such as testing and simulation can only provide a partial verification of behavior in critical real-time software systems, and thus, formal verification is an alternative to complement these activities. Two useful formal software verification approaches are deductive verification and abstract interpretation, which analyze programs statically to identify defects. This paper explores abstract interpretation and deductive verification by employing Frama-C's value analysis and Jessie plug-ins to verify embedded aerospace control software. The results indicate that both approaches can be employed in a software verification process to make software more reliable.
Description
Keywords
Citation