Industrial Projects - Revision history

imported>Andy: /* ADVANCE EU Project */

2015-10-23T11:40:39Z

ADVANCE EU Project

← Older revision		Revision as of 11:40, 23 October 2015
Line 8:		Line 8:
	http://www.advance-ict.eu/industry_days including:		http://www.advance-ict.eu/industry_days including:
	* '''AWE''' - Co-Design Architecture (CODA)		* '''AWE''' - Co-Design Architecture (CODA)
	* '''Thales (~~Austria~~)''' - Railway Interlocking models		* '''Thales (Germany)''' - Railway Interlocking models
	* '''Selex ES''' - Smart-grid modelling		* '''Selex ES''' - Smart-grid modelling
	* '''Critical Software''' Smart-grid modelling		* '''Critical Software''' Smart-grid modelling

imported>Andy: /* Industrial Projects and Research Projects using Event-B */

2015-10-23T11:38:52Z

Industrial Projects and Research Projects using Event-B

@@ Line 1: / Line 1: @@
-=Industrial Projects and Research Projects using Event-B=
+=Industrial Use: Projects and Research Projects using Event-B=
 === From partners within the DEPLOY Project ===
@@ Line 35: / Line 51: @@
 * [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>

imported>Sascha: /* Industrial Projects and Research Projects using Event-B */

2012-08-09T09:38:47Z

Industrial Projects and Research Projects using Event-B

← Older revision		Revision as of 09:38, 9 August 2012
Line 6:		Line 6:
	* '''Siemens Transportation''' have been working on train control and signalling systems		* '''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)		* '''Space Systems Finland''' have been working on part of the BepiColombo space probe and on Attitude and Orbit Control System software(AOCS)
	* '''SAP''' ~~are~~ working on analysis of business choreography models		* '''SAP''' have been working on analysis of business choreography models
	* '''Systerel''' are working on railway and aerospace systems		* '''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

imported>Sascha: /* Industrial Projects and Research Projects using Event-B */

2012-08-09T09:38:03Z

Industrial Projects and Research Projects using Event-B

imported>WikiSysop: /* DSF Project, Japan */

2012-05-11T13:41:40Z

DSF Project, Japan

← Older revision		Revision as of 13:41, 11 May 2012
Line 41:		Line 41:

	=== DSF Project, Japan ===		=== 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.]		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.]

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

imported>WikiSysop: /* DSF Project, Japan */

2012-05-11T13:41:31Z

DSF Project, Japan

← Older revision		Revision as of 13:41, 11 May 2012
Line 41:		Line 41:

	=== DSF Project, Japan ===		=== 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.]

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

imported>WikiSysop at 13:41, 11 May 2012

2012-05-11T13:41:08Z

← Older revision		Revision as of 13:41, 11 May 2012
Line 36:		Line 36:
	* [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.		* [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.

	=== ADVANCE Project ===		=== ADVANCE EU Project ===

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

			=== DSF Project, Japan ===

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

imported>Sascha: /* From non-Deploy partners */

2012-05-03T08:26:59Z

From non-Deploy partners

← Older revision		Revision as of 08:26, 3 May 2012
Line 32:		Line 32:

	* [[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/].		* [[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.

	=== ADVANCE Project ===		=== ADVANCE Project ===

imported>WikiSysop at 16:36, 11 October 2011

2011-10-11T16:36:53Z

← Older revision		Revision as of 16:36, 11 October 2011
Line 33:		Line 33:
	* [[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/].		* [[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/].

			=== ADVANCE Project ===

			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.

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

imported>Steve at 11:18, 29 September 2011

2011-09-29T11:18:31Z

← Older revision		Revision as of 11:18, 29 September 2011
Line 31:		Line 31:


	* [[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/].


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

← Older revision		Revision as of 09:38, 9 August 2012
Line 1:		Line 1:
	=Industrial Projects and Research Projects using Event-B=		=Industrial Projects and Research Projects using Event-B=

	=== From partners within the ~~Deploy~~ Project ===		=== 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:		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		* '''Bosch''' have been working on developing a cruise control system and a start-stop system
	* '''Siemens Transportation''' ~~are~~ working on train control and signalling systems		* '''Siemens Transportation''' have been working on train control and signalling systems
	* '''Space Systems Finland''' ~~are~~ working on part of the BepiColombo space probe		* '''Space Systems Finland''' have been working on part of the BepiColombo space probe and on Attitude and Orbit Control System software(AOCS)
	* '''SAP''' are working on analysis of business choreography models		* '''SAP''' are working on analysis of business choreography models
	* '''Systerel''' are working on railway and aerospace systems		* '''Systerel''' are working on railway and aerospace systems
Line 18:		Line 18:
	*:: [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 partners of the ~~Deploy~~ Project ===		=== From partners of the DEPLOY Project ===
	Following ~~Deploy~~ partners are involved in other projects related to using Event-B and Rodin:		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.		* '''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 ===		=== 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