Automated development of computerized interlocking systems
- Safety Errors are eliminated using formal safety verification
- Speed Reliable systems are generated by the push of a button, and are easier to certify, maintain and update
- Savings Development resources are minimized by extensive reuse and automation
Prover iLock is a tool suite that automates development of computerized interlocking systems.
With Prover iLock, it is possible to develop an interlocking system in one day, on an average computer, including:
- Generation of code for both vital and non-vital logic, and distributed systems
- Safety verification using 100% coverage formal proof
- Functional testing with co-simulation of the system and environment models
- Generation of documentation
- Reuse of test cases for hardware-in-the-loop testing
- CENELEC SIL 4-compliant process
Development flow
The Prover iLock process is based on using a Generic Application formally specified in PiSPEC.
This is reused for development and V&V of a large number of Specific Applications. Based on the Specific Application Configuration, Prover iLock generates the design, the safety requirements and the test cases.
The design is detailed enough to be automatically translated to software code. The safety requirements are used to verify that the system will always be safe. The test cases are used for functional testing of that the system behaves as expected.
Product modules
Different product modules are used in the Prover iLock development flow.
Prover iLock Base controls the system under development, and provides the built-in layout editor for creating the Specific Application Configuration. This defines the system's track layout, configuration settings for individual wayside objects, speed restriction data and so on. The configuration can also be imported from file.
Prover iLock Verifier performs formal verification of all safety requirements at the push of a button. Formal verification means that mathematical proof is used to ensure that the system fulfils the requirements, providing 100 % coverage verification.
Prover iLock Simulator performs functional testing of all test cases at the push of a button. The simulator has a powerful debugger and also supports interactive simulation.
Prover iLock Coder generates software code for the system at the push of a button. The Coder module supports leading interlocking platforms, as well as generation of code in the programming language C.
Prover iLock Documenter generates documentation for the system, including control tables and forms for factory and commissioning tests.
