Software for Rail Control
Prover Trident – for today’s more complex digital train control
Meeting the higher demands for capacity is a major challenge for the railway industry. The ability to deliver rail infrastructure both fast and cost-efficiently is a critical success factor. A common bottleneck in such projects is the development and safety assessment of rail control software for the digital railway. Whether applied for new installations, upgrades of existing ones, traditional interlockings, ERTMS or CBTC — this calls for dedicated software tools designed for the task.
Our contribution is Prover Trident;
a complete process and tool suite that reduces engineering efforts and life cycle costs, provide prompt time-to-market and ensures certification to the highest available safety standards. Prover Trident is based on the combined use of the following three solutions: PiSPEC IP, Prover iLock and Prover Certifier.
PiSPEC IP
PiSPEC is a formal specification language designed to facilitate formalization and review of requirement specifications for railway signaling systems, and to enable automated engineering and verification of such systems. PiSPEC is used to formalize design, test and safety specifications.
Prover iLock
Prover iLock is a desktop tool for development of application software for railway interlocking systems. Prover iLock automatically turns PiSPEC IP together with an application configuration into revenue service code for the given target hardware, complete with functional test and safety verification reports.
Prover Certifier
Prover Certifier is a sign-off verification tool, creating CENELEC EN50128 SIL 4 compliant safety evidence for the Specific Application software based on formal verification. Prover Certifier minimizes the need for traditional safety verification tasks such as testing and code review.
ADDITIONAL SOLUTIONS
Prover Extractor
Prover Extractor is a tool for automated processing, checking and generation of Relay-Based Interlocking system schematics. It is used to extract component and interconnection data from relay circuit schematic drawings. This enables checking design consistency and conformance to design guidelines, and formal verification of Relay-Based Interlocking systems.
Prover SL CE
PSL with its library Prover SL CE is a model checker capable of formally verifying big industrial systems. For valid properties it produces a proof log that can be checked by an independent checker. For falsified properties it produces a counterexample and provides powerful built-in debugging aid.