About Prover iLock
Prover iLock is a desktop tool for producing fully documented, tested and verified application software for railway interlocking systems, ready for compilation and installation on the target platform. Given the signaling rules captured in a PiSPEC IP specification and the configuration of a specific interlocking, Prover iLock instantiates the requirements formalized by the PiSPEC IP for the scenarios and objects in the configured application. Prover iLock can then automatically:
- turn the instantiated requirements into revenue service code,
- formally verify that the code meets the safety requirements,
- test the functionality using simulation and
- document the application and produce test instructions for installation testing.
Prover iLock consists of the following software modules
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 in the verification.
Prover iLock Simulator
performs functional testing of all test cases at the push of a button. The simulator has a powerful debugger and supports also interactive simulation, with visualization and control of the simulation in the graphical representation of the track layout.
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, test and verification reports as well as forms for factory and commissioning tests.
These modules can be used together or separately, though that the base model is required to use any of the other modules. When used without the Prover iLock Coder module the other modules can be used to analyze code that has been developed outside of Prover iLock, in a code import flow.
Prover iLock Coder
Prover iLock Coder generates software code for system designs created in Prover iLock. This eliminates the need to write software code by hand, freeing up resources from signaling engineers enabling them to perform other work where their skills are put to better use.
Prover iLock Coder benefits:
- Consistent software code across different applications
- Efficient code (with code optimization applied)
- Efficient validation of resource usage
- Higher code quality compared to manually written code
Prover iLock Coder supports generation of code for both vital systems and non-vital systems and has a flexible framework in which code generators for different target languages can be combined. The generation process produces all the necessary configuration files and data, including interfaces to adjacent systems and wayside objects, and scripts for compiling the generated code. Code can be generated for both centralized and distributed interlocking systems. For distributed systems, Prover iLock Coder generates the configuration of the communication links, including communication variables transmitted.
Prover iLock Coder supports a number of proprietary languages and interlocking platforms as well as a standard C-code generator for use with commercial off-the-shelf hardware. Support for additional interlocking targets and communication protocols can be added as needed.
Prover iLock Documenter
Prover iLock Documenter generates documentation for Specific Applications. The document generation capabilities are configurable, making it easy to adapt to different documentation needs.
Typical documentation of Specific Applications includes:
- Lists of wayside objects
- Tables of the routes and their protection areas
- Logical formulas detailing the interlocking conditions used
- Specifications of required testing activities for installation
- Checklists adapted to the Specific Application configuration
With Prover iLock Documenter you generate these documents automatically ones the Specific Application has been configured. While in a traditional process the production of documentation requires substantial effort, it is quick and easy in a Prover iLock Process, as Prover iLock Documenter does it for you. Writing detailed documents such as test plans by hand is also tedious and error prone, with Prover iLock Documenter you are guaranteed consistent results.
Prover iLock Documenter is highly customizable to your personal needs. You can include data from any step in the development and V&V process and present it in different file formats such as:
- Text (.txt)
- Comma separated spreadsheet (.csv)
- Microsoft Office Excel (.xls or .xlsx)
- Microsoft Office Word (.doc or .docx)
Prover iLock Simulator
Prover iLock Simulator provides efficient simulation of large sets of test cases, generated from generic PiSPEC definitions, against system designs created in Prover iLock. Simulation of external code, imported into Prover iLock, is also supported. The simulation is time-compressed, which is considerably faster than execution on the target hardware platform. This makes it efficient to determine the functional correctness of a system during development, reduces development time and lets engineers spend their time more productively. All test cases and simulation results obtained can be exported, enabling hardware-in-the-loop testing to repeat all desktop simulation results.
The Simulator supports distributed systems, as well as both vital and non-vital code. The execution models in a distributed system can be mixed, making it possible to make a very accurate simulation of a distributed interlocking system with communication links, remote office control systems, environment models (simulating behavior of wayside objects) and multiple platforms.
Prover iLock Simulator has a powerful built-in debugger, which makes it efficient to pin-point the cause of failing test cases, and to visualize the system’s behavior. Simulation can also be interactive, where the user can control the input to the system from the graphical user interface of Prover iLock, and directly observe the response from the system.
Prover iLock Simulator benefits:
- Efficient and accurate simulation of multiple interlocking platforms
- Supports both automated testing of test cases generated from PiSPEC IP and more traditional manually testing
- Easy to use, built in debugger with ladder logic viewer and graphical visualization of the simulation state
- Multiple interlocking systems can be connected and simulated together
Prover iLock Verifier
Prover iLock Verifier provides efficient formal verification of safety requirements against system designs created in Prover iLock. Verification of external code, imported into Prover iLock, is also supported.
Formal verification is based on automatic proof search, and provides 100% verification coverage against forbidden, unsafe states: if the system under verification can reach any state that violates a safety requirement, Prover iLock Verifier detects and reports this, including the sequence of events leading to this state.
The built-in debugger provides efficient support for identifying why the system allows entering a forbidden, unsafe state. Formal verification is strongly recommended for safety verification by standards such as CENELEC EN 50128, and encouraged or even mandated by a growing number infrastructure managers. Prover iLock Verifier provides automated, easy-to-use formal verification with unparalleled speed and capacity, ensuring predictable formal verification results for your interlocking systems.
Proven formal verification technology with unparalleled capacity & performance
Prover iLock Verifier is based on the market leading technology for safety verification of critical embedded systems, which has been proven by use in industries such as avionics, Electronic Design Automation, automotive and railway signaling.
Prover iLock Verifier provides the speed & capacity required to provide exhaustive formal verification of some of the largest interlocking systems in the world in just a few hours of CPU computation time. Prover Technology has invested more than 250 man-years of R&D in formal verification technology such as SAT-based model checking, abstraction, and interpolation. Prover iLock Verifier combines such verification methods with various strengths and weaknesses to provide unparalleled performance and capacity.
Prover Trident is a complete process and tool suite for interlocking design automation. Unlike other point tools, Prover Trident covers the whole life-cycle for interlocking software.
PiSPEC is a formal specification language for defining signalling principles for interlocking software, consisting of object model, design principles, test and safety principles. The principles for a specific system type is called PiSPEC IP.
Prover Certifier is an independent tool for sign-off verification of revenue service code, producing CENELEC EN 50128 SIL-4 compliant evidence. Verification results from Prover Certifier can be used as the sole safety evidence, making manual safety tests and code reviews superfluous.