Abstract
This paper presents an approach to construct a verified virtual protoyping 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and ARM multiprocessor machine code. In: DAMP 2009, pp. 13–24. ACM, New York (2008)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer (2004)
Bobot, F., Filliâtre, J., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. Boogie 53–64, 2011 (2011)
Campbell, B.: An executable semantics for CompCert C. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 60–75. Springer, Heidelberg (2012)
Canet, G., Cuoq, P., Monate, B.: A value analysis for C programs. In: SCAM 2009, pp. 123–124. IEEE (2009)
Coq Development Team. The Coq Reference Manual, Version 8.2. INRIA Rocquencourt, France (2008). http://coq.inria.fr/
Filliâtre, J.-C., Marché, C.: The why/krakatoa/caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)
Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243–258. Springer, Heidelberg (2010)
Hao, H., Song, J., Helmstetter, C., Joloboff, V.: Generation of executable representation for processor simulation with dynamic translation. In: Proceedings of the International Conference on Computer Science and Software Engineering, Wuhan, China. IEEE (2008)
Helmstetter, C., Joloboff, V., Xiao, H.: SimSoC: a full system simulation software for embedded systems. In: IEEE (ed.) 2009 IEEE International Workshop on Open-source Software for Scientific Computation (OSSC), pp. 49–55, Sept 2009
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: sel4: Formal verification of an os kernel. In: Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207–220. ACM, New York (2009)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
Leroy, X.: The CompCert C verified compiler. Documentation and user’s manual. INRIA Paris-Rocquencourt, March 2012
Monin, J.-F., Shi, X.: Handcrafted inversions made operational on operational semantics. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 338–353. Springer, Heidelberg (2013)
Pusch, C.: Proving the soundness of a java bytecode verifier specification in isabelle/HOL. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 89. Springer, Heidelberg (1999)
Sutarwala, S., Paulin, P.G., Kumar, Y.: Insulin: An instruction set simulation environment. In: CHDL 1993: 11th IFIP WG10.2 International Conference, pp. 369–376. North-Holland, Amsterdam (1993)
Witchel, E., Rosenblum, M.: Embra: fast and flexible machine simulation. In: SIGMETRICS 1996, pp. 68–79. ACM, New York (1996)
Zhu, J., Gajski, D.D.: An ultra-fast instruction set simulator. IEEE Trans. Very Large Scale Integr. Syst. 10(3), 363–373 (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Joloboff, V., Monin, JF., Shi, X. (2015). Towards Verified Faithful Simulation. In: Li, X., Liu, Z., Yi, W. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2015. Lecture Notes in Computer Science(), vol 9409. Springer, Cham. https://doi.org/10.1007/978-3-319-25942-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-25942-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-25941-3
Online ISBN: 978-3-319-25942-0
eBook Packages: Computer ScienceComputer Science (R0)