EB2C : A Tool for Event-B to C Conversion Support

Dominique Méry 1 Neeraj Kumar Singh 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : To use of formal model effectively in formal method based development process, it is highly desirable that the formal specification be converted to C code, a de facto standard in many industrial application domains, such as medical, avionics and automotive control. In this paper we present the design methodology of a tool that translates an Event-B formal specification to equivalent C code with proper correctness assurance.
Document type :
Other publications
Complete list of metadatas

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/inria-00540006
Contributor : Neeraj Kumar Singh <>
Submitted on : Monday, February 21, 2011 - 5:49:59 PM
Last modification on : Thursday, September 19, 2019 - 5:00:14 PM
Long-term archiving on : Tuesday, November 6, 2012 - 2:30:40 PM

File

cameraready-sefm2010.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00540006, version 1

Collections

Citation

Dominique Méry, Neeraj Kumar Singh. EB2C : A Tool for Event-B to C Conversion Support. 2010. ⟨inria-00540006⟩

Share

Metrics

Record views

279

Files downloads

608