Skip to Main content Skip to Navigation
Book sections

Towards Verified Faithful Simulation

Abstract : This paper presents an approach to construct a verified virtual prototyping framework of embedded software. The machine code executed on a simulated target architecture can be proven to provide the same results as the real hardware, and the proof is verified with a theorem prover. The method consists in proving each instruction of the instruction set independently, by proving that the execution of the C code simulating an instruction yields an identical result to that obtained by a formal executable model of the processor architecture. This formal model itself is obtained through an automated translation process from the architecture specifications. Each independent proof draws a number of lemmas from a generic lemma library and also uses the automation of inversion tactics in the theorem prover. The paper presents the proof of the ARM architecture version 6 Instruction Set Simulator of the SimSoC open source simulator, with all of the proofs being verified by the Coq proof assistant, using automated tactics to reduce manual proof development.
Complete list of metadata
Contributor : Vania Joloboff Connect in order to contact the contributor
Submitted on : Friday, December 11, 2015 - 9:39:14 AM
Last modification on : Thursday, February 3, 2022 - 11:18:24 AM




Vania Joloboff, Jean-François Monin, Xiaomu Shi. Towards Verified Faithful Simulation. Xuandong Li, Zhiming Liu, Wang Yi. Dependable Software Engineering: Theories, Tools, and Applications, Springer, pp.315, 2015, Lecture Notes in Computer Science, ISBN 978-3-319-25942-0. ⟨10.1007/978-3-319-25942-0⟩. ⟨hal-01241837⟩



Record views