Difference between revisions of "Industrial Projects"

From Event-B
Jump to navigationJump to search
imported>Nicolas
imported>Tommy
m
Line 1: Line 1:
 
=Industrial Projects and Research Projects using Event-B=
 
=Industrial Projects and Research Projects using Event-B=
  
* In the [http://www.deploy-project.eu/ Deploy Project] several industrial partners are using Event-B and Rodin on deployment projects:
+
=== From partners within Deploy Project ===
** Bosch are working on a cruise control system
+
In the [http://www.deploy-project.eu/ Deploy Project] several industrial partners are using Event-B and Rodin on deployment projects:
** Siemens Transportation are working on train control and signalling systems
+
* '''Bosch''' are working on a cruise control system
** Space Systems Finland are working on part of the BepiColombo space probe
+
* '''Siemens Transportation''' are working on train control and signalling systems
** SAP are working on analysis of business choreography models
+
* '''Space Systems Finland''' are working on part of the BepiColombo space probe
** Systerel are working on railways and aerospace applications
+
* '''SAP''' are working on analysis of business choreography models
**:* ''DIR 41 Case Study - How Event-B Can Improve an Industrial System Specification''
+
* '''Systerel''' are working on railways and aerospace applications
**:: Christophe Metayer and  Mathieu Clabaut
+
*:* ''DIR 41 Case Study - How Event-B Can Improve an Industrial System Specification''
**:: Abstract State Machine, B and Z 2008, Springer Verlag, LNCS 5238
+
*:: Christophe Metayer and  Mathieu Clabaut
**:: [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]
+
*:: Abstract State Machine, B and Z 2008, Springer Verlag, LNCS 5238
**:* ''Formal Data Validation - Formal Techniques Applied to Verification of Data Properties.''  
+
*:: [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]
**:: Mathieu Clabaut, Christophe Metayer, and Éric Morand  
+
*:* ''Formal Data Validation - Formal Techniques Applied to Verification of Data Properties.''  
**:: Embedded Real Time Software and Systems 2010, Toulouse.
+
*:: Mathieu Clabaut, Christophe Metayer, and Éric Morand  
**:: [http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010%202/ERTS2010_0158_final.pdf ERTS2010_0158_final.pdf]
+
*:: 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
  
* [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.
  
* [[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



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.