@inproceedings{6cecf8ecb6884474add13c1adbc4dd72,
title = "Formal verification of a rover anti-collision system",
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.",
keywords = "Bounded model checking, Equivalence proof, Inductive proof, S3, SAT, Safety critical system, Test case generation",
author = "Ning Ge and Eric Jenn and Nicolas Breton and Yoann Fonteneau",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 21st International Workshop on Formal Methods for Industrial Critical Systems, FMICS-AVoCS 2016 and 16th International Workshop on Automated Verification of Critical Systems, AVoCS 2016 ; Conference date: 26-09-2016 Through 28-09-2016",
year = "2016",
doi = "10.1007/978-3-319-45943-1\_12",
language = "英语",
isbn = "9783319459424",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "171--188",
editor = "\{ter Beek\}, \{Maurice H.\} and Stefania Gnesi and Alexander Knapp",
booktitle = "Critical Systems",
address = "德国",
}