Mars 15th-17th 2010, Tokyo, Japan
Presentation
The aim of this workshop is to illustrate B/event-B formal modeling as a technique for specifying, designing, coding and validating software-based systems.
Backed with the two main open-source modeling platforms (RODIN, Atelier B) and in relation with the growing number of industrial applications in the Railways and in the Smartcard domains, this workshop is headed at providing a clear picture of B/Event-B current status of development and exploitation, focusing on the support tools as well as the industrial applications. The workshop includes a large scope of presentations given by the DEPLOY project members or associated to the project results.
Target audience is software/system engineers and project managers, as well as researchers in the domain.
Program
Discover the Event report
Session 1
- The Big Picture (T. Lecomte)
- System-level modeling with Event B (M. Butler)
- The Rodin platform (M. Butler)
Session 2
- Model checking and animation with ProB (M. Leuschel)
- UML-B (M. Butler)
- Code generation (T. Lecomte / A. Requet)
- Sequential code in C / Ada
- PLCs
- VHDL
Session 3
- Automatic refinement (A. Requet)
- Industrial applications
- Automatic pilots (Siemens, Alstom): (T. Lecomte)
- Validation of large scale railway models: (M. Leuschel)
- Event-B in space (Space System Finland case study)
- Smartcard (Memory Protection Unit from STMicroelectronics): (T. Lecomte)