Industrial Projects

Industrial Projects and Research Projects using Event-B

From partners within Deploy Project

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

From non-Deploy partners

• 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.