Industrial deployment of system engineering methods providing high dependability and productivity


About Deploy Project


Workpackage 2 Deployment in the transportation sector


Increasingly rail transportation systems use high degrees of software automation for both safety and control. The main concern of Siemens Transportation in DEPLOY is demonstrating the safety of the rail systems that they develop, in particular the safety of products that are reused in different operational contexts. Modifying a safe pre-existing system can lead to many unsafe scenarios that are hard to detect, especially at a system level. We believe that refinement-based formal engineering methods will enable us to manage the complexity of ensuring system safety and maintaining safety during system modification and customisation. These methods will also provide us with the evidence to demonstrate safety to a high level of assurance.

Siemens are currently industrialising their TrainGuard Communications Based Train Control (CBTC) system. TrainGuard will make a major contribution to future interoperability of European rail systems. In WP2, we will deploy formal engineering methods to the control function of TrainGuard. This is a large safety-critical system that includes both on-board and wayside components. TrainGuard will be reused in several projects, with some modifications and customisations. We will have to demonstrate that the generic system is safe and that any modifications of the system do not compromise safety. Key to this effort will be ensuring that environmental and equipment assumptions are properly represented in our formal models.

Objectives of WP2

  • DEPLOY refinement-based formal engineering methods to ensure and demonstrate system-level safety of Siemens rail signalling product. Key to this is ensuring that we can properly model appropriate environmental assumptions, particularly fault assumptions.
  • Develop effective ways of using these methods to ensure and demonstrate preservation of safety of modified and customised signalling product.
  • DEPLOY modelling and analysis tools that fit well with the development processes used by Siemens rail safety engineers and that support the construction of safety cases. This includes tools that support the graphical representation of system models.
  • Provide a link with our existing formal processes for software construction including code generation tools.

Description of work

The work of WP2 will be organised according to the following tasks:

Tasks T2.1-T2.2 on Technology Transfer: Siemens has considerable experience of applying formal methods to software components of railway systems. For DEPLOY the challenge is to raise this to the level of overall systems in order to address system safety and for this they require some additional training and support. During the deployment activities we will identify methodological and tooling challenges to feed back to WP6-WP8 (Methodological R&D) and WP9 (Tooling R&D).

Tasks T2.3-T2.5 on Deployment: The deployment will be on a system-based development of the control functionality of the TrainGuard CBTC. This will involve detailed requirements specification followed by formal development of the system which will treat on-board and wayside functionality and all relevant environmental assumptions. We will have an initial pilot deployment on a subset of the system functionality. This will feed into initial work on safety under reuse and on software construction. T2.5 will then undertake an enhanced deployment on the full system functionality. Siemens has two priority challenges that need to be addressed in DEPLOY. The first is maintaining safety of a system when it is modified and reused for a different operational context. The second to be able to integrate the formal developments used for system-level modelling and analysis with our existing process for automated construction of executable code from formal models of software components.

Tasks T2.6-T2.8 on Method Assessment and Integration: These tasks will investigate the impact and cost-effectiveness of deploying formal engineering methods to rail signalling system development, especially in safety assurance. We will develop a strategy for integration of the methods in Siemens system development processes which need to conform to the CENELEC safety standards. To help us, RATP (Paris Metro authority), a major rail operator with considerable experience of formal methods, will provide an assessment of how well the methods conform to the development standards that they require. RATP are a subcontractor to Siemens in DEPLOY.

Deploy-Project - All right reserved