PiSPEC is a formal language dedicated for signaling engineering. It enables you to specify Generic Applications from which Specific Applications can be automatically generated by the push of a button, resulting in software code for an interlocking platform of the user's choice.
With PiSPEC you can also specify safety requirements and functional requirements generically, allowing you to verify and simulate each generated Specific Application to check that it is safe and fully functional.
PiSPEC is developed to be the perfect interface between signaling engineers and signaling automation tools such as Prover iLock. You can express yourself in a natural way, which simplifies validation and maintenance.
Particular care has been taken to make language features self-explanatory. In fact, the reviewer of a PiSPEC specification need not have any programming experience - it is much more important that the reviewer is an expert on signaling principles.
PiSPEC builds on standard concepts that are taught in engineering classes all over the world. It originates from predicate logic, but has been enhanced with a strict type system that helps discovering flaws and omissions already during the writing of the specification.
To aid the organization of code, an object orientation paradigm is provided, with classes, inheritance and interfaces. Access control mechanisms make it easy to understand what kind of consequences changes can have, which is particularly useful during development and maintenance of large PiSPEC libraries.
One can organize PiSPEC specifications in libraries. It is often convenient to base the PiSPEC specifications on a standard library from Prover Technology, such as the AREMA package.
PiSPEC is particularly suited for development of certified software. Automatically generated Specific Applications can be certified according to CENELEC SIL 4 using Prover Certifier.