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