Software Tool Suite for Automated Control and Signaling Engineering

Prover iLock is a software product with several extension modules for engineering of control and signaling applications. It has an unparalleled track record when it comes to cutting costs, ensuring safe operation, and speeding up the development process. With the product, Prover Technology has pioneered and integrated industry changing capabilities like

• Generic formal specifications (PiSPEC)
• CENELEC SIL-4 certifiable formal safety verification with proof
  logging and independent proof checking capabilities
• Automatic generation of application code, test suites and safety
  properties from high level application configuration data
• Hardware-accurate co-simulation of centralized or distributed
  non-vital and vital applications

The core Prover iLock product enables application engineers to quickly create Application Configurations. An Application Configuration typically consists of a track layout, distribution and zoning information, and various other application specific data. Based on this high level data and the PiSPEC libraries, Prover iLock generates Application Safety, Test and Design Specifications.

The Prover iLock modules operate on the generated Application Specifications, and automate coding, simulation and formal safety verification. Once the PiSPEC libraries have been developed and validated, new applications can be engineered in hours. This cuts costs and frees up critical engineering resources for other tasks.

Verifier Module

The Verifier Module is used to formally verify that the Application Code is unable to enter any of the unsafe states specified in the Application Safety Specification. The tool uses a combination of diversification, proof logging and independent proof checking to ensure compliance with CENELEC SIL-4.

Simulator Module

The Simulator Module is used to validate that the Application Code complies with the test sequences listed in the Application Test Specification. This type of testing may take weeks, months or years on the physical hardware. Using the Simulator Module’s time compressed execution, it is accomplished in hours. Then, when it is time for field testing, the Application Code is certain to pass all logic tests.

Coder Module

The Coder Module reads a target-independent Application Design Specification and generates Application Code for a variety of targets, including VHLC, MicroLok and ANSI-C. This eliminates the need to write application specific code manually. Instead, the signaling engineers devote their time to developing generic re-usable PiSPEC libraries.