Industrial Projects: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Nicolas |
imported>Nicolas |
||
| Line 7: | Line 7: | ||
* '''Space Systems Finland''' are working on part of the BepiColombo space probe | * '''Space Systems Finland''' are working on part of the BepiColombo space probe | ||
* '''SAP''' are working on analysis of business choreography models | * '''SAP''' are working on analysis of business choreography models | ||
* '''Systerel''' are working on | * '''Systerel''' are working on railway and aerospace systems | ||
*: they are using Event-B to specify models of train controlers and signalling 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'' | *:* ''DIR 41 Case Study - How Event-B Can Improve an Industrial System Specification'' | ||
Revision as of 14:51, 18 March 2011
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
- they are using Event-B to specify models of train controlers and signalling systems
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.
