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 the 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.
Author supplied keywords
Cite
CITATION STYLE
Ge, N., Jenn, E., Breton, N., & Fonteneau, Y. (2016). Formal verification of a rover anti-collision system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9933 LNCS, pp. 171–188). Springer Verlag. https://doi.org/10.1007/978-3-319-45943-1_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
