On two Friends for getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin

Abstract : We report on our progress-to-date in implementing a software de- velopment environment which integrates the efforts of two formal software engineering techniques: program refinement as supported by Event B and program verification as supported by the Spec# programming system. Our objective is to improve the usability of formal verification tools by providing a general framework for integrating these two approaches to software veri- fication. We show how the two approaches Correctness-by-Construction and Post-hoc Verification can be used in a productive way. Here, we focus on the final steps in this process where the final concrete specification is transformed into an executable algorithm. We present EB2RC,a plug-in for the Rodin platform, that reads in an Event B model and uses the control framework introduced during its refinement to generate a graphical representation of the executable algorithm. EB2RC also generates a recursive algorithm that is eas- ily translated into executable code. We illustrate our technique through case studies and their analysis.
Type de document :
Communication dans un congrès
Bernhard Steffen and Tiziana Margaria. ISOLA 2016 , Oct 2016, CORFU, Greece. Springer, I (9952), pp.18, 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 〈10.1007/978-3-319-47166-2_57〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01369425
Contributeur : Dominique Méry <>
Soumis le : mercredi 21 septembre 2016 - 08:03:21
Dernière modification le : mercredi 22 novembre 2017 - 11:02:25

Identifiants

Collections

Citation

Dominique Méry, Rosemary Monahan, Cheng Zheng. On two Friends for getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin. Bernhard Steffen and Tiziana Margaria. ISOLA 2016 , Oct 2016, CORFU, Greece. Springer, I (9952), pp.18, 2016, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 〈10.1007/978-3-319-47166-2_57〉. 〈hal-01369425〉

Partager

Métriques

Consultations de la notice

242