OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Formal Verification of a Rover Anti-collision System

Ge, Ning and Jenn, Eric and Breton, Nicolas and Fonteneau, Yoann Formal Verification of a Rover Anti-collision System. (2016) In: FMICS-AVoCS 2016, 26 September 2016 - 28 September 2016 (Pisa, Italy).

(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/978-3-319-45943-1_12


In this paper, we integrate inductive proof, bounded model checking, test case generation and equivalence proof techniques to verify an embedded system. This approach is implemented using Systerel Smart Solver (S3) toolset. It is applied to verify properties at system, software, and code levels. The verification process is illustrated on an anti-collision system (ARP for Automatic Rover Protection) implemented on-board a rover. Focus is placed on the verification of safety and functional properties and the proof of equivalence between the design model and the generated code.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer. The original PDF of the article can be found on SpringerLink: https://link.springer.com/chapter/10.1007/978-3-319-45943-1_12
HAL Id:hal-01649511
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Other partners > Thales (FRANCE)
Other partners > IRT Saint Exupéry - Institut de Recherche Technologique (FRANCE)
Other partners > SYSTEREL (FRANCE)
Deposited On:27 Nov 2017 14:30

Repository Staff Only: item control page