Transforming EVENT B Models into Verified C# Implementations

Dominique Méry 1, 2, * Monahan Rosemary 3
* Auteur correspondant
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The refinement-based approach to developing software is based on the correct-by-construction paradigm where software systems are constructed via the step-by-step refinement of an initial high- level specification into a final concrete specification. Proof obligations, generated during this process are discharged to ensure the consistency between refinement levels and hence the system's overall correctness. Here, we are concerned with the refinement of specifications using the EVENT B modelling lan- guage and its associated toolset, the RODIN platform. In particular, we focus on the final steps of the process where the final concrete specification is transformed into an executable algorithm. The transformations involved are (a) the transformation from an EVENT B specification into a concrete recursive algorithm and (b) the transformation from the recursive algorithm into its equivalent itera- tive version. We prove both transformations correct and verify the correctness of the final code in a static program verification environment for C# programs, namely the Spec# programming system.
Type de document :
Communication dans un congrès
Alexei Lisitsa and Andrei Nemytykh. VPT 2013 - First International Workshop on Verification and Program Transformation, Jul 2013, Saint Petersburg, Russia. 16, pp.57-73, 2013, EPIC. 〈http://www.easychair.org/publications/?page=692335489〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00862050
Contributeur : Dominique Méry <>
Soumis le : dimanche 15 septembre 2013 - 21:01:25
Dernière modification le : jeudi 11 janvier 2018 - 06:25:25

Identifiants

  • HAL Id : hal-00862050, version 1

Collections

Citation

Dominique Méry, Monahan Rosemary. Transforming EVENT B Models into Verified C# Implementations. Alexei Lisitsa and Andrei Nemytykh. VPT 2013 - First International Workshop on Verification and Program Transformation, Jul 2013, Saint Petersburg, Russia. 16, pp.57-73, 2013, EPIC. 〈http://www.easychair.org/publications/?page=692335489〉. 〈hal-00862050〉

Partager

Métriques

Consultations de la notice

306