Automates development and V&V of interlocking software
- Signal principles tailored for North American railroads
- Automatic code generation
- Automatic safety verification
- Automatic functional testing (simulation)
- Generation of test sheets for FAT and SAT testing
- Supports interlocking platforms such as MicroLok II, VHLC and ElectroLogIXS
- Supports coded track circuits: Electro Code and MicroTrax
Prover iLock for American Railroads is an off-the-shelf solution for development of software for interlocking systems.
It is based on the Prover iLock Process, and consists of and a Generic Application tailored for North American railroads.
With Prover iLock, it is possible to develop complex interlocking systems in one day, on an average computer, including:
- Generation of code for both vital and non-vital logic, supporting distributed systems
- Safety verification with 100 % coverage
- Functional testing with co-simulation of the system and environment models
- Generation of documentation and tables for factory and on-site testing
(Click to enlarge screenshot)
Process
The process is based on a Generic Application (GA), defining the signaling principles both informally, in English, as well as in PiSPEC, a formal language for signaling engineering.
It captures design and safety requirements as well as generic test cases. The GA has been developed by Prover Technology in close collaboration with Canadian Pacific Railway. The GA can easily be adjusted to the meet specific needs of other North American railroads.
Using the Generic Application the effort of coding, documenting and testing the software for a Specific Application (SA) is reduced to simple configuration of the system in Prover iLock. The main parts of the configuration is the track layout, which is drawn directly in the Prover iLock graphical editor, and additional data typically found in route and aspect charts, such as mapping of signal aspects to track codes.
Generated code
The exact format of the generated code depends on the platform that is targeted, but it is always complete with both equations and IO mappings for all the programs, both vital and non-vital.
The GA has been designed so that the generated equations shall look familiar to signaling engineers, and it is possible to browse and inspect them directly in the built-in ladder logic viewer of Prover iLock as well as in the tools provided by the target platform vendors. This reduces the training effort needed when deploying the solution.
