Simulator Semantics for System Level Formal Verification

Toni Mancini
(Computer Science Department - Sapienza University of Rome)
Federico Mari
(Computer Science Department - Sapienza University of Rome)
Annalisa Massini
(Computer Science Department - Sapienza University of Rome)
Igor Melatti
(Computer Science Department - Sapienza University of Rome)
Enrico Tronci
(Computer Science Department - Sapienza University of Rome)

Many simulation based Bounded Model Checking approaches to System Level Formal Verification (SLFV) have been devised. Typically such approaches exploit the capability of simulators to save computation time by saving and restoring the state of the system under simulation. However, even though such approaches aim to (bounded) formal verification, as a matter of fact, the simulator behaviour is not formally modelled and the proof of correctness of the proposed approaches basically relies on the intuitive notion of simulator behaviour. This gap makes it hard to check if the optimisations introduced to speed up the simulation do not actually omit checking relevant behaviours of the system under verification.

The aim of this paper is to fill the above gap by presenting a formal semantics for simulators.

In Javier Esparza and Enrico Tronci: Proceedings Sixth International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), Genoa, Italy, 21-22nd September 2015, Electronic Proceedings in Theoretical Computer Science 193, pp. 86–99.
Published: 23rd September 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.193.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org