From Event-B to Verified C via HLL

Preprint English OPEN
Ge , Ning; Dieumegard , Arnaud; Jenn , Eric; Voisin , Laurent;
  • Publisher: HAL CCSD
  • Subject: S3 | C | Code generation | Property proof | [ INFO.INFO-SE ] Computer Science [cs]/Software Engineering [cs.SE] | HLL | [ INFO.INFO-PF ] Computer Science [cs]/Performance [cs.PF] | Event-B | [ INFO.INFO-SC ] Computer Science [cs]/Symbolic Computation [cs.SC] | Computer Science - Software Engineering | Equivalence proof

This work addresses the correct translation of an Event-B model to C code via an intermediate formal language, HLL. The proof of correctness follows two main steps. First, the final refinement of the Event-B model, including in-variants, is translated to HLL. At that po... View more
  • References (33)
    33 references, page 1 of 4

    1. Jean-Raymond Abrial. Modeling in Event-B: system and software engineering. Cambridge University Press, 2010.

    2. Jean-Raymond Abrial and Jean-Raymond Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 2005.

    3. Mike Barnett, K Rustan M Leino, and Wolfram Schulte. The spec# programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pages 49-69. Springer, 2004.

    4. Dirk Beyer, Thomas A Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker blast. International Journal on Software Tools for Technology Transfer, 9(5-6):505- 525, 2007.

    5. Armin Biere, Cyrille Artho, and Viktor Schuppan. Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science, 66(2):160-177, 2002.

    6. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. Springer, 1999.

    7. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009.

    8. Per Bjesse and Koen Claessen. SAT-based verification without state space traversal. In Formal Methods in Computer-Aided Design, pages 409-426. Springer, 2000.

    9. Pontus Boström. Creating sequential programs from event-b models. In International Conference on Integrated Formal Methods, pages 74-88. Springer, 2010.

    10. Pontus Boström, Fredrik Degerlund, Kaisa Sere, and Marina Waldén. Derivation of concurrent programs by stepwise scheduling of event-b models. Formal Aspects of Computing, 26(2):281-303, 2014.

  • Similar Research Results (4)
  • Metrics
Share - Bookmark