First steps towards the certification of an ARM simulator using Compcert

Xiaomu Shi 1 Jean-François Monin 1, 2 Frederic Tuong 1 Frédéric Blanqui 1
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : The simulation of Systems-on-Chip (SoC) is nowadays a hot topic because, beyond providing many debugging facilities, it allows the development of dedicated software before the hardware is available. Low-consumption CPUs such as ARM play a central role in SoC. However, the effectiveness of simulation depends on the faithfulness of the simulator. To this effect, we propose here to prove significant parts of such a simulator, SimSoC. Basically, on one hand, we develop a Coq formal model of the ARM architecture while on the other hand, we consider a version of the simulator including components written in Compcert-C. Then we prove that the simulation of ARM operations, according to Compcert-C formal semantics, conforms to the expected formal model of ARM. Size issues are partly dealt with using automatic generation of significant parts of the Coq model and of SimSoC from the official textual definition of ARM. However, this is still a long-term project. We report here the current stage of our efforts and discuss in particular the use of Compcert-C in this framework.
Type de document :
Communication dans un congrès
First International Conference on Certified Programs and Proofs, Dec 2011, Hengchun, Taiwan. 7086, 2011, LNCS. 〈10.1007/978-3-642-25379-9_25〉
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00624833
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 29 février 2012 - 03:04:58
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 13 décembre 2016 - 19:43:32

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xiaomu Shi, Jean-François Monin, Frederic Tuong, Frédéric Blanqui. First steps towards the certification of an ARM simulator using Compcert. First International Conference on Certified Programs and Proofs, Dec 2011, Hengchun, Taiwan. 7086, 2011, LNCS. 〈10.1007/978-3-642-25379-9_25〉. 〈inria-00624833〉

Partager

Métriques

Consultations de la notice

488

Téléchargements de fichiers

179