Industrial Projects: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Nicolas
imported>Andy
 
(13 intermediate revisions by 5 users not shown)
Line 1: Line 1:
=Industrial Projects and Research Projects using Event-B=
=Industrial Use: 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:
=== ADVANCE EU Project ===
* '''Bosch''' are working on a cruise control system
 
* '''Siemens Transportation''' are working on train control and signalling systems
Southampton, Dusseldorf, Systerel, Alstom and Critical Software Technologies are partners in the [http://www.advance-ict.eu/ FP7 ADVANCE Project].  The overall objective of ADVANCE is the development of a unified tool-based framework for automated formal verification and simulation-based validation of cyber-physical systems. In ADVANCE, Rodin is being further strengthened and augmented with novel approaches to multi-simulation and testing.
* '''Space Systems Finland''' are working on part of the BepiColombo space probe
 
* '''SAP''' are working on analysis of business choreography models
http://www.advance-ict.eu/industry_days including:
* '''Systerel''' are working on railways and aerospace applications
* '''AWE''' - Co-Design Architecture (CODA)
* '''Thales (Germany)''' - Railway Interlocking models
* '''Selex ES''' - Smart-grid modelling
* '''Critical Software''' Smart-grid modelling
 
=== DSF Project, Japan ===
 
The Dependable Systems Forum (DSF) project involves several Japanese Companies namely NTT-Data, Fujitsu, Hitachi, NEC, Toshiba, and SCSK.  The DSF project applied several formal methods including Event-B and Rodin to an industrial development. [http://wiki.event-b.org/images/RodinJapan.pdf  Further details are here.]
 
 
=== From partners within the DEPLOY Project ===
In the [http://www.deploy-project.eu/ DEPLOY Project] several industrial partners are using Event-B and Rodin on deployment projects:
* '''Bosch''' have been working on developing a cruise control system and a start-stop system
* '''Siemens Transportation''' have been working on train control and signalling systems
* '''Space Systems Finland''' have been working on part of the BepiColombo space probe and on Attitude and Orbit Control System software(AOCS)
* '''SAP''' have been 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
*: 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''
Line 18: Line 34:
*:: [http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010%202/ERTS2010_0158_final.pdf ERTS2010_0158_final.pdf]
*:: [http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010%202/ERTS2010_0158_final.pdf ERTS2010_0158_final.pdf]


=== From non-Deploy partners ===  
=== From partners of the DEPLOY Project ===
Following DEPLOY partners are involved in other projects related to using Event-B and Rodin:
* '''Newcastle University''' is involved in the UK [http://safecap.cs.ncl.ac.uk/index.php/Safecap_Project_Wiki SafeCap Project] on developing modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained. The project team (Newcastle University, Swansea University, Invensys Rail) works on integrating proof-based reasoning about time in state-based models, exemplified by Event-B and CSP-Prover, and on providing an open tool support for verifying timed systems. SafeCap is supported by EPSRC and RSSB.
 
=== 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:
* [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 deadman control for trains
Line 27: Line 47:




* [[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] used 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. The results of the project are available at [http://deploy-eprints.ecs.soton.ac.uk/346/].
 


* [http://www.qnx.com/ '''QNX Software Systems Limited'''], a leading vendor of operating systems, development tools, and professional services for connected embedded systems, is applying the Rodin tools to the design of software for a simple medical device. The aim is to use the evidence provided by the tool to support a safety case and to help in the approval process.


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

Latest revision as of 11:40, 23 October 2015

Industrial Use: Projects and Research Projects using Event-B

ADVANCE EU Project

Southampton, Dusseldorf, Systerel, Alstom and Critical Software Technologies are partners in the FP7 ADVANCE Project. The overall objective of ADVANCE is the development of a unified tool-based framework for automated formal verification and simulation-based validation of cyber-physical systems. In ADVANCE, Rodin is being further strengthened and augmented with novel approaches to multi-simulation and testing.

http://www.advance-ict.eu/industry_days including:

  • AWE - Co-Design Architecture (CODA)
  • Thales (Germany) - Railway Interlocking models
  • Selex ES - Smart-grid modelling
  • Critical Software Smart-grid modelling

DSF Project, Japan

The Dependable Systems Forum (DSF) project involves several Japanese Companies namely NTT-Data, Fujitsu, Hitachi, NEC, Toshiba, and SCSK. The DSF project applied several formal methods including Event-B and Rodin to an industrial development. Further details are here.


From partners within the DEPLOY Project

In the DEPLOY Project several industrial partners are using Event-B and Rodin on deployment projects:

  • Bosch have been working on developing a cruise control system and a start-stop system
  • Siemens Transportation have been working on train control and signalling systems
  • Space Systems Finland have been working on part of the BepiColombo space probe and on Attitude and Orbit Control System software(AOCS)
  • SAP have been 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 partners of the DEPLOY Project

Following DEPLOY partners are involved in other projects related to using Event-B and Rodin:

  • Newcastle University is involved in the UK SafeCap Project on developing modelling techniques and tools for improving railway capacity while ensuring that safety standards are maintained. The project team (Newcastle University, Swansea University, Invensys Rail) works on integrating proof-based reasoning about time in state-based models, exemplified by Event-B and CSP-Prover, and on providing an open tool support for verifying timed systems. SafeCap is supported by EPSRC and RSSB.

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



  • QNX Software Systems Limited, a leading vendor of operating systems, development tools, and professional services for connected embedded systems, is applying the Rodin tools to the design of software for a simple medical device. The aim is to use the evidence provided by the tool to support a safety case and to help in the approval process.

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.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Industrial_Projects&oldid=5680’