PiSPEC is a formal language dedicated for signaling engineering. It enables you to specify signaling requirements in a clear and formal way and to package this as reusable PiSPEC IP.
PiSPEC is developed to be the perfect interface between signaling engineers and signaling automation tools such as Prover iLock. You can express requirements in a natural way, thus simplifying validation and maintenance. Care has been taken to make language features self-explanatory.
PiSPEC builds on standard concepts that are taught in engineering classes all over the world. It originates from predicate logic, enhanced with a strict type system and object orientation. The type system helps discovering many flaws and omissions already during the writing of the specification. The object orientation supplies classes, inheritance and interfaces, that adds structure to the specifications and provides a natural way to modelling any signaling system. PiSPEC IP can also be structured into libraries that further facilitates reuse.
When using PiSPEC together with Prover iLock a test-driven approach to the development of the specifications is encouraged and supported by the tool. You can develop design, test and safety requirements in parallel and try them out on reference applications configured in Prover iLock, with instant feedback.
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.
Prover iLock is a tool suite for configuration, generation and checking of applications based on PiSPEC IP. Creating revenue service code and V&V results based on simulation and formal safety verification is accomplished using push-button tools.
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.