On Wednesday 28 November 2012, 10:00-10:30 INRIA Lille room B31 (new building), Nestor Catano (The University of Madeira) will give a talk on “Code Generation for Reactive Systems”
Abstract: Event-B provides a formal language notation for the modelling and development of Reactive Systems. The notation is supported by the Rodin platform, an open-source Eclipse IDE that provides a set of tools for working with Event-B models, e.g. an editor, a proof generator, (semi-) automatic provers, and a model-checking animator. I will present an ongoing work on code generation for Event-B models and discuss how I envision to extend this work to support the code generation of Interactive Systems. Code generation begins with an abstract Event-B model for the particular system. The model can be refined (and associated refinement proof obligations discharged in Rodin) as needed to add more functionality, but the goal of these refinements is not to bring the model closer to code level as would normally be done in an Event-B development process with Rodin. Rather, once a refinement that includes adequate functionality is achieved, it is translated to a JML (short for Java Modeling Language) class specification. Then, Java reactive code for this specification is automatically generated from the JML specification.
