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.
Type de document :
Chapitre d'ouvrage
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〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01241837
Contributeur : Vania Joloboff <>
Soumis le : vendredi 11 décembre 2015 - 09:39:14
Dernière modification le : jeudi 11 janvier 2018 - 06:21:19

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

132