Difference between revisions of "Industrial Projects"
From Event-B
Jump to navigationJump to searchimported>Nicolas m (→Industrial Projects and Research Projects using Event-B: added Systerel) |
imported>Tommy m |
||
Line 1: | Line 1: | ||
=Industrial Projects and Research Projects using Event-B= | =Industrial Projects and Research Projects using Event-B= | ||
− | + | === From partners within 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 |
− | * | + | * '''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 railways and aerospace applications | |
− | + | *:* ''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 | |
− | + | *:: [http://books.google.fr/books?id=WI6_MrPlTz4C&lpg=PA357&ots=PmjR-nbOfZ&dq=DIR%2041%20Case%20Study%20How%20Event-B%20Can%20Improve%20an%20Industrial%20System%20Specification&pg=PA357#v=onepage&q=DIR%2041%20Case%20Study%20How%20Event-B%20Can%20Improve%20an%20Industrial%20System%20Specification&f=false 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. | |
+ | *:: [http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010%202/ERTS2010_0158_final.pdf ERTS2010_0158_final.pdf] | ||
+ | === From non-Deploy partners === | ||
+ | * [http://www.grupo-aes.com.br/site/home/ '''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 | ||
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
+ | * [[User:Steve| Steve Wright]], [http://www.cs.bris.ac.uk/~eder/ Kerstin Eder] and [http://www.cs.bris.ac.uk/~henkm/ Henk Muller] are using Event-B at [http://www.xmos.com/ '''XMOS Ltd'''] in Bristol under a [http://www.epsrc.ac.uk/funding/grants/business/Pages/knowledgetransfersecondments.aspx KTS] (Grant EP/H500316/1), applying the methods of the [http://dx.doi.org/10.1007/978-3-540-87603-8_21 MIDAS] project to the [http://www.xmos.com/technology/xcore XCore] embedded microprocessor. | ||
− | |||
− | + | <span style="color:#006400">'''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.'''</span> | |
− | 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. |
Revision as of 14:25, 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 railways and aerospace applications
- 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.