Difference between revisions of "Industrial Projects"

From Event-B
Jump to navigationJump to search
imported>WikiSysop
imported>Nicolas
Line 6: Line 6:
 
** 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 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]
  
  

Revision as of 14:09, 18 March 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 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


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