Revision as of 15:05, 10 August 2011

Industrial Projects and Research Projects using Event-B

In the Deploy Project several industrial partners are using Event-B and Rodin on deployment projects:

Bosch are working on a cruise control system
Siemens Transportation are working on train control and signalling systems
Space Systems Finland are working on part of the BepiColombo space probe
SAP are working on analysis of business choreography models
Systerel are working on railway and aerospace systems
they are using Event-B to specify models of train controlers and signalling systems
- DIR 41 Case Study - How Event-B Can Improve an Industrial System Specification
Christophe Metayer and Mathieu Clabaut

Abstract State Machine, B and Z 2008, Springer Verlag, LNCS 5238

B_2008.pdf
- Formal Data Validation - Formal Techniques Applied to Verification of Data Properties.
Mathieu Clabaut, Christophe Metayer, and Éric Morand

Embedded Real Time Software and Systems 2010, Toulouse.

ERTS2010_0158_final.pdf

Academic partners are involved in other projects related to using Event-B and Rodin:

Newcastle University is involved in a UK project SafeCap on developing modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained. The project team (Newcastle University, Swansea University, Invensys Rail) works on integrating proof-based reasoning about time in state-based models, exemplified by Event-B and CSP-Prover, and on providing an open tool support for verifying timed systems

AeS Group in Brazil are using Event-B and Rodin on Railway related projects:
Analysis of deadman control for trains

Analysis of a safety critical hardware verification function (by software)

Requirements adaptation

Validation of Formal Specification

Also, internship positions are open to work in industry applying Formal Methods. Please contact Dinho (agrj@aes.com.br) or Thiago (thiago@aes.com.br) to discuss about ongoing projects

Steve Wright, Kerstin Eder and Henk Muller are using Event-B at XMOS Ltd in Bristol under a KTS (Grant EP/H500316/1), applying the methods of the MIDAS project to the XCore embedded microprocessor.

If you are using Event-B and Rodin on an industrial or research project, please feel free to add a short description and a link to this page.

@@ Line 1: / Line 1: @@
 =Industrial Projects and Research Projects using Event-B=
-=== From partners within Deploy Project ===
+=== From partners within the Deploy Project ===
 In the [http://www.deploy-project.eu/ Deploy Project] several industrial partners are using Event-B and Rodin on deployment projects:
 * '''Bosch''' are working on a cruise control system
@@ Line 17: / Line 17: @@
 *:: Embedded Real Time Software and Systems 2010, Toulouse.
 *:: [http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010%202/ERTS2010_0158_final.pdf ERTS2010_0158_final.pdf]
+=== From partners of the Deploy Project ===
+Academic partners are involved in other projects related to using Event-B and Rodin:
+* '''Newcastle University''' is involved in a UK project SafeCap on developing modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained. The project team (Newcastle University, Swansea University, Invensys Rail) works on integrating proof-based reasoning about time in state-based models, exemplified by Event-B and CSP-Prover, and on providing an open tool support for verifying timed systems
 === From non-Deploy partners ===