In our previous blog post, we looked at some of the challenges commonly faced in delivery of rail control projects and proposed a remedy: the use of detailed and clear requirement specifications that enables automated development and more efficient safety verification. We will now take a closer look at this process for signaling systems design and how it is implemented with Prover Trident for automation. Our vision is that delivery of rail control systems shall be standardized, with:
- Clearly defined requirements as generic principles, used with automation tools
- Efficient management of new/changed requirements during life cycle
- Automated development gives efficient, safe and predictable results
- Safety acceptance based on sign-off verification against the Infrastructure Managers safety requirements
- Computing components (hardware) that easily can be replaced with other brands (future proof); open interfaces enable product replacements
We recommend that the Infrastructure Managers provide tender specifications that separate life cycles of the hardware and software and encourage the use of automated development processes and formal safety verification. The suppliers are then well equipped to apply a Signal Systems Design process, to meet the expectations of the Infrastructure Managers, and to maximize business benefits:
- Speed: Increase delivery capacity, and ensure that delivery schedules are met
- Safety: Provide safety verification with 100% coverage, that is easy to repeat
- Savings: Reduce dependency on labor intense, error-prone, manual development processes
A signaling systems design solution
Prover’s implementation of the signaling system design process is called Prover Trident. A three-pronged process that automates development, test and safety verification:
Formal Specification, defining a Generic Application (GA) for the signaling principles, as formalized requirement specifications in the PiSPEC language.
Automated Development, using Prover iLock to configure, generate, simulate and formally verify the application software for Specific Applications (SAs).
Sign-off Verification, using Prover Certifier to create CENELEC EN50128 SIL 4-compliant safety evidence for the application software based on formal verification.
Prover Trident is a complete development process for generation, test and verification of revenue service signaling software, but it can also be used for prototyping in the requirement capturing phase, to simulate and test different requirements both at component and system levels.
Benefits of a solution for signaling systems design
The main benefits of using Prover Trident for automated development and safety assessment of interlocking application software are:
- Significantly reduced engineering effort and time to market.
- Significantly reduced life cycle costs, with efficient management of requirement changes during the life cycle of the system (maintenance).
- Efficient CENELEC EN50128 SIL 4 compliance in safety assessment.
- Predictable project schedules, with high quality deliveries.
- An efficient, automated process for producing SA safety case, based on formal verification.
- Reduced dependency on a single supplier; it is easy to use the same design solution and process for multiple interlocking platforms. Avoids vendor lock-in and increases competition.
Generic and specific applications
In the context of Prover Trident, a Generic Application (GA) refers to a set of general signalling principles and requirements, formalized in the PiSPEC language. The GA is structured the following way:
- Object Model (OM), the specification of the objects, including their parameters and interfaces.
- Generic Application Configuration (GAC), generic definition of configuration formats.
- Generic Design Specification (GDS), the design requirements to implement.
- Generic Safety Specification (GSS), the safety requirements to verify.
- Generic Test Specification (GTS), the test cases to simulate for testing the functionality (positive behavior) of the specific applications.
These specifications are developed in natural language versions (typically English) and formal versions. The formalization is done in the PiSPEC language, with additional configuration scripts implemented in the Python scripting language.
The GA is used to automatically develop Specific Applications (SAs), for instance an interlocking system for a given signal location. With the GA in place the effort to develop an SA is reduced to a simple configuration task, either directly using the GUI of Prover iLock or by importing the configuration from an existing database.
Functional testing, safety verification and code generation is then fully automated, and the full process, including configuration, doesn’t have to take more than a few hours. During the GA development, Prover iLock is used to validate the requirements on a set of typical SAs, in an iterative and test-driven approach.
Demonstration of Application Engineering with Prover iLock
Interested in learning more about Prover Trident, and how Prover iLock is used to develop revenue service interlocking software? Sign up for our webinar ‘Demonstration of an Interlocking Design Automation Solution’, or watch a shorter recorded product demonstration here.