Verify, detect and report in seconds
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 market-leading model checker PSL 4 for safety verification of critical embedded systems. PSL 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 complete formal verification of some of the largest interlocking systems in the world in just a few hours of CPU computation time. Prover 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 to provide unparalleled performance and capacity.
Automated Code Generation
Optimized, Consistent, and High-Quality Code
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 cod
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.
Automated Document Generation
Quick, Consistent, and Adaptable Documentation
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)
Efficient System Simulation
Time-Compressed Testing and Powerful Debugging Tools
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