Prover Extractor – Relay-Based Interlocking (RBI) System Schematics 2017-09-22T14:15:47+00:00

Prover Extractor

For Automated Processing, Checking and Generation of Relay-Based Interlocking (RBI) System Schematics

About Prover Extractor

Prover Extractor is a product for automated processing, checking and generation of Relay-Based Interlocking (RBI) system schematics. A main feature of the product is to extract component and interconnection data from relay circuit schematic drawings. This enables checking design consistency and conformance to design guidelines, and to perform formal verification of Relay-Based Interlocking systems.

Prover Extractor supports Bentley’s Microstation DGN format, and is applied for checking and development of some of the largest Relay-Based Interlocking systems in operation today, maintained by Trafikverket in Sweden.

Benefits & Usage

  • Automated checking of design guidelines improves maintainability of RBI schematics
  • Automated generation of wiring, rack and cabling diagrams saves cost and time for RBI system assembly
  • Automated generation of component database and change management saves time and cost
  • Computerized checks and generation improves quality and consistency for complex RBI systems
  • Formal verification of safety requirements against RBI system improves quality and saves time and cost
  • Cross-check of RBI schematics against components database saves time and cost

Click to enlarge the screenshots

Component list, showing relay contact RSS933- with clips 17/18

Wiring diagram, showing wire from RSS933-/18 to RS903FII/17

Configuration, symbols can be added and configured

Change control management, showing wires and components to add/remove

Component database, showing all contacts for relay RSS933- in schematics and in database


PiSPEC is a formal specification language for defining signalling principles for interlocking software, consisting of object model, design principles, test and safety principles. The principles for a specific system type is called PiSPEC IP.

Find out more

Prover iLock

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.

Find out more

Prover Certifier

Prover Certifier is an independent tool for sign-off verification of revenue service code, producing CENELEC EN 50128 SIL-4 compliant evidence. Verifi­cation results from Prover Certifier can be used as the sole safety evidence, making manual safety tests and code reviews superfluous.

Find out more

By continuing to use the site, you agree to the use of cookies. More information

The cookie settings on this website are set to "allow cookies" to give you the best browsing experience possible. If you continue to use this website without changing your cookie settings or you click "Accept" below then you are consenting to this. To find out more, visit