title = {{Towards Verified Faithful Simulation} },
    author = {Joloboff, Vania and Monin, Jean-Fran\c{c}ois and Shi, Xiaomu},
    year = {2015},
    booktitle = {Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, {SETTA} 2015, Nanjing, China, November 4-6, 2015, Proceedings},
    pages = {105--119},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    volume = {9409},
    team = {PACSS},
    pdf = {Docs/setta15.pdf},
    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.},

Publication Sections

Contact | Site Map | Site powered by SPIP 3.0.26 + AHUNTSIC [CC License]

info visites 817990