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 896kB |
Official URL: https://doi.org/10.1007/978-3-319-45943-1_12
Abstract
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) |
| Statistics: | download |
| Deposited On: | 27 Nov 2017 14:30 |
Repository Staff Only: item control page
