More Web Proxy on the site http://driver.im/

research-article

Automatic code generation from event-B models

Authors:

Dominique Méry,

Neeraj Kumar SinghAuthors Info & Claims

SoICT '11: Proceedings of the 2nd Symposium on Information and Communication Technology

Pages 179 - 188

https://doi.org/10.1145/2069216.2069252

Published: 13 October 2011 Publication History

Abstract

This paper presents a translation tool that automatically generates efficient target programming language code (C, C++, Java and C#) from Event-B formal specification related to the analysis of complex problems. This tool is a collection of plug-ins, which are used for translating Event-B formal specifications into different kinds of programming languages. The translation tool is rigorously developed with safety properties preservation. The results detailed in this paper are an architecture of the translation process, to generate a target language code from Event-B models using Event-B grammar through syntax-directed translation, code scheduling architecture and verification of an automatic generated code. The translator checks syntax and type consistency before generating the target programming language code. The translation tool has been developed as a set of Rodin plug-ins under the Eclipse development framework. An assessment of the proposed approach is given through a case study, relative to the development of a cardiac pacemaker system.

References

[1]

J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press.

Digital Library

[2]

J.-R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, New York, NY, USA, 1996.

[3]

Ken Arnold, James Gosling, and David Holmes. The Java Programming Language (Fourth Edition). Addison-Wesley Professional, 2005.

Digital Library

[4]

Atelier B. Atelier de génie logiciel permettant de développer des logiciels prouvés sans défaut. http://www.atelierb.eu/.

[5]

S. Serge Barold, Roland X. Stroobandt, and Alfons F. Sinnaeve. Cardiac Pacemakers Step by Step. Futura Publishing, 2004. ISBN 1-4051-1647-1.

[6]

Marco Bernardo and Edoardo Bontà. Generating well-synchronized multithreaded programs from software architecture descriptions. In WICSA, pages 167--176, 2004.

Digital Library

[7]

Marco Bernardo and Edoardo Bontà. Preserving architectural properties in multithreaded code generation. In COORDINATION, LNCS, pages 188--203, 2005.

Digital Library

[8]

Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, and Laurent Voisin. Adaptable Translator of B Specifications to Embedded C Programs. In FME, pages 94--113, 2003.

[9]

Dirk Beyer, Thomas Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker BLAST, Applications to software engineering. STTT, 9:505--525, 2007.

Digital Library

[10]

Dines Bjørner and Cliff B. Jones, editors. The Vienna Development Method: The Meta-Language, London, UK, 1978. Springer-Verlag.

[11]

E. Bonta and M. Bernardo. PADL2Java: A Java code generator for process algebraic architectural descriptions. In Software Architecture, 2009 European Conference on Software Architecture. WICSA/ECSA 2009., pages 161--170, 2009.

[12]

Carlos Paiz Christopher Pohl and Mario Porrmann. vMAGIC-Automatic Code Generation for VHDL. In International Journal of Reconfigurable Computing.

[13]

D. Coleman and J. W. Hughes. The clean termination of Pascal programs. Acta Informatica, 11:195--210, 1979. 10.1007/BF00289066.

Digital Library

[14]

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. Combination of abstractions in the astrée static analyzer. In Proceedings of the 11th Asian computing science conference on Advances in computer science: secure software and related issues, ASIAN'06, pages 272--300, Berlin, Heidelberg, 2007. Springer-Verlag.

Digital Library

[15]

EB2ALL. Automatic code generation from Event-B to many Programming Languages. http://eb2all.loria.fr/, 2011.

[16]

Andrew Edmunds and Michael Butler. Tool Support for Event-B Code Generation. In WS-TBFM2010, February 2010.

[17]

Andrew Edmunds and Michael Butler. Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In PLACES 2011, February 2011.

[18]

James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. Java(TM) Language Specification, The (3rd Edition). Addison-Wesley Professional, 2005.

Digital Library

[19]

Brian W. Kernighan and Dennis Ritchie. C Programming Language. Prentice Hall, 1988. ISBN-100131103628.

Digital Library

[20]

Dominique Méry and Neeraj Kumar Singh. Pacemaker's Functional Behaviors in Event-B. Research Report (http://hal.inria.fr/inria-00419973/en/), 2009.

[21]

Dominique Méry and Neeraj Kumar Singh. EB2C: A Tool for Event-B to C Conversion Support, Poster and Tool Demo submission and published in a CNR Technical Report in SEFM. 2010.

[22]

Dominique Méry and Neeraj Kumar Singh. Technical Report on Formal Development of Two-Electrode Cardiac Pacing System. (http://hal.archives-ouvertes.fr/inria-00465061/en/), 2010.

[23]

Dominique Méry and Neeraj Kumar Singh. Functional behavior of a cardiac pacing system. International Journal of Discrete Event Control Systems, 1(2):129--149, 2011.

[24]

Overture Tool Box. Overture: Formal Modelling in VDM. http://www.overturetool.org/.

[25]

David J. Pearce, Paul H. J. Kelly, and Chris Hankin. Efficient field-sensitive pointer analysis of c. ACM Trans. Program. Lang. Syst., 30(1):4, 2007.

Digital Library

[26]

Project RODIN. Rigorous open development environment for complex systems. http://rodin-b-sharp.sourceforge.net/, 2004.

[27]

Jeffrey Richter. CLR Via C#, Second Edition. Microsoft Press, Redmond, 2006.

[28]

Richard L. Sites. Clean Termination of Computer Programs. Ph.D. dissertation, Stanford University, Stanford, California, June 1974.

Digital Library

[29]

Jeffrey E. Smith, Mieczyslaw M. Kokar, and Kenneth Baclawski. Formal verification of uml diagrams: A first step towards code generation. In The Unified Modeling Language, pages 224--240. GI, 2001.

Digital Library

[30]

Bjarne Stroustrup. The C++ Programming Language, Third Edition. Addison-Wesley, 1994.

Digital Library

[31]

Steve Wright. Automatic Generation of C from Event-B. In Workshop on Integration of Model-based Formal Methods and Tools IMFMT'2009 -- in IFM'2009, Düsseldorf, Germany.

Cited By

Rivière PSingh NAït-Ameur Y(2024)Reflexive Event-B: Semantics and Correctness the EB4EB FrameworkIEEE Transactions on Reliability10.1109/TR.2022.321964973:2(835-850)Online publication date: Jun-2024
https://doi.org/10.1109/TR.2022.3219649
Ammar SSakka Rouis TBhiri M(2024)A correct-by-construction approach for development of reliable planning problemsJournal of Logic and Computation10.1093/logcom/exae016Online publication date: 2-Apr-2024
https://doi.org/10.1093/logcom/exae016
Martins Gomes RAichernig BBaunach M(2024)A framework for embedded software portability and verification: from formal models to low-level codeSoftware and Systems Modeling10.1007/s10270-023-01144-y23:2(289-315)Online publication date: 1-Feb-2024
https://doi.org/10.1007/s10270-023-01144-y
Show More Cited By

Recommendations

Code generation for Event-B

Event-B is a modelling language and a formal methods approach for correct construction of software. This paper presents our work on code generation for Event-B, including the definition of a syntactic translation from Event-B to JML-annotated Java ...
Towards the Composition of Specifications in Event-B

The development of a system can start with the creation of a specification. Following this viewpoint, we claim that often a specification can be constructed from the combination of specifications which can be seen as composition. Event-B is a formal ...
VHDL Code Generation from Formal Event-B Models
DSD '11: Proceedings of the 2011 14th Euromicro Conference on Digital System Design

In this paper, we present an approach that allows to generate VHDL code from formal models developed with the Event-B formalism. The approach is based on the relationship between the structure of the formal model and hardware description language ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SoICT '11: Proceedings of the 2nd Symposium on Information and Communication Technology

October 2011

225 pages

ISBN:9781450308809

DOI:10.1145/2069216

General Chairs:
Thang Huynh Quyet
Hanoi University of Science and Technology, Vietnam
,
Dinh Khang Tran
Hanoi University of Science and Technology, Vietnam

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SoICT '11

SoICT '11: Symposium on Information and Communication Technology 2011

October 13 - 14, 2011

Hanoi, Vietnam

Acceptance Rates

Overall Acceptance Rate 147 of 318 submissions, 46%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

61
Total Citations
View Citations
685
Total Downloads

Downloads (Last 12 months)49
Downloads (Last 6 weeks)6

Reflects downloads up to 14 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Rivière PSingh NAït-Ameur Y(2024)Reflexive Event-B: Semantics and Correctness the EB4EB FrameworkIEEE Transactions on Reliability10.1109/TR.2022.321964973:2(835-850)Online publication date: Jun-2024
https://doi.org/10.1109/TR.2022.3219649
Ammar SSakka Rouis TBhiri M(2024)A correct-by-construction approach for development of reliable planning problemsJournal of Logic and Computation10.1093/logcom/exae016Online publication date: 2-Apr-2024
https://doi.org/10.1093/logcom/exae016
Martins Gomes RAichernig BBaunach M(2024)A framework for embedded software portability and verification: from formal models to low-level codeSoftware and Systems Modeling10.1007/s10270-023-01144-y23:2(289-315)Online publication date: 1-Feb-2024
https://doi.org/10.1007/s10270-023-01144-y
Schellhorn GBodenmüller SReif W(2024)VeriCode: Correct Translation of Abstract Specifications to C CodeIntegrated Formal Methods10.1007/978-3-031-76554-4_4(53-74)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_4
Leuschel M(2024)Specifications are Preferably Amenable to Proof and AnimationThe Practice of Formal Methods10.1007/978-3-031-66676-6_14(271-291)Online publication date: 4-Sep-2024
https://doi.org/10.1007/978-3-031-66676-6_14
Pinna GRavalico DRovito LManzoni LDe Lorenzo A(2024)Enhancing Large Language Models-Based Code Generation by Leveraging Genetic ImprovementGenetic Programming10.1007/978-3-031-56957-9_7(108-124)Online publication date: 28-Mar-2024
https://doi.org/10.1007/978-3-031-56957-9_7
Bouba KAit Wakrime AOuhammou YBenaini R(2023)A transformation methodology for Capella to Event-B models with DSL verificationJournal of Computer Languages10.1016/j.cola.2023.10124177(101241)Online publication date: Nov-2023
https://doi.org/10.1016/j.cola.2023.101241
Karmakar R(2023)A graphical tool for formal verification using Event-B modelingMultimedia Tools and Applications10.1007/s11042-023-15993-883:4(10899-10923)Online publication date: 24-Jun-2023
https://doi.org/10.1007/s11042-023-15993-8
Rivière PSingh NAït-Ameur YDupont G(2023)Standalone Event-B Models Analysis Relying on the EB4EB Meta-theoryRigorous State-Based Methods10.1007/978-3-031-33163-3_15(193-211)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33163-3_15
Singh NAït‐Ameur YMendil IMéry DNavarre DPalanque PPantel M(2023)F3FLUIDJournal of Software: Evolution and Process10.1002/smr.243935:7Online publication date: 2-Jul-2023
https://dl.acm.org/doi/10.1002/smr.2439
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents