Prover Technology - Accelerating Development and Reducing Cost of Provably Correct Rail Control Systems

Prover iLock is the leading software solution for control and signalling application design, verification, validation, optimisation and documentation. It has been deployed by hardware suppliers and operators in more than 25 countries. Prover iLock has an unparallelled track record when it comes to cutting costs, ensuring safe operation and speeding up the development process.

The core Prover iLock product automatically generates complete application design, test and safety specifications for a signalling application. It does this from a generic application-independent configuration data package and a high level specification that includes a track plan.

Prover iLock also includes functionality for debugging, document generation, and import of code, relay systems and control tables.

PROVER ILOCK CODER

Prover iLock Coder automatically generates application code from the application design specification. This completely eliminates the need to write application code by hand.

The coding effort is instead spent on the generic re-usable configuration data packages. Prover iLock Coder supports generation of centralised and distributed code, including IO and board set-up files. For typical partner hardware, it generates a ladder logic format read by the partner compiler. Contact us for a list of partners.

PROVER ILOCK VERIFIER

Prover iLock Verifier formally verifies that the application code meets all applicable safety requirements. It models the partner hardware, the application code and the application safety specification, and then applies automated mathematical proof searches. There is no need to write a single test. If an unsafe scenario violating a requirement exists, Prover iLock Verifier will find it, generate the corresponding test and display it in the debugger. The engineer then pin-points and fixes the unsafe logic and re-runs the tool.

PROVER ILOCK SIMULATOR

Prover iLock Simulator enables signalling engineers to rapidly determine whether the application code meets its operational and functional requirements. Testing time is shortened significantly through accelerated emulation of the partner hardware.

Prover iLock Simulator flags all expect statements that the application code fails to meet. The signalling engineer then launches the debugger to pinpoint and fix logic errors in the generic design specification (or, if the application was imported, the code or relay system).

PROVER ILOCK STABILIZER

Prover iLock Stabilizer enables signalling engineers to perform stability verification and optimisation at the push of a button. It builds up a model of the partner hardware, application code, execution order and input constraints, and then initiates analysis.

If an input sequence causing oscillation exists, Prover iLock Stabilizer finds and displays it. If no such sequence exists, it generates a modified execution order that reaches a stable state in as few cycles as possible without altering application behaviour.