OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Integrated formal verification of safety-critical software

Ge, Ning and Jenn, Eric and Breton, Nicolas and Fonteneau, Yoann Integrated formal verification of safety-critical software. (2017) International Journal on Software Tools for Technology Transfer. 1 - 18. ISSN 1433-2779

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/s10009-017-0475-0


This work presents a formal verification process based on the Systerel Smart Solver (S3) toolset for the development of safety-critical embedded software. In order to guarantee the correctness of the implementation of a set of textual requirements, the process integrates different verification techniques (inductive proof, bounded model checking, test case generation and equivalence proof) to handle different types of properties at their best capacities. It is aimed at the verification of properties at system, design, and code levels. To handle the floating-point arithmetic (FPA) in both the design and the code, an FPA library is designed and implemented in S3. This work is illustrated on an Automatic Rover Protection (ARP) system implemented on-board a robot. Focus is placed on the verification of safety and functional properties and on the equivalence proof between the design model and the generated code.

Item Type:Article
Additional Information:Thanks to Springer Verlag editor. The original PDF of the article can be found at https://link.springer.com/article/10.1007/s10009-017-0475-0?wt_mc=Internal.Event.1.SEM.ArticleAuthorOnlineFirst#citeas
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:Other partners > Thales (FRANCE)
Other partners > Beihang University (CHINA)
Other partners > IRT Saint Exupéry - Institut de Recherche Technologique (FRANCE)
Other partners > SYSTEREL (FRANCE)
Deposited On:21 Feb 2018 10:48

Repository Staff Only: item control page