Prover Extractor

Software Product for Relay-Based Interlocking systems

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:

  • Checking that schematics conform to RBI design guidelines
  • Generating formal verification model for RBI schematics
  • Generating wiring, rack and cabling diagrams for RBI assembly
  • Generating and checking that schematics conform to external component database
  • Support for automated detailing of RBI schematics
  • Support for version and change control management of RBI schematics
  • Configurable symbolic library supports multiple styles of RBI schematics

Benefits and usage:

  • Automated checking of design guidelines improve 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

Find out more here: Case Studies - Trafikverket (Swedish Transport Administration)



(Click to enlarge screenshots)
Highslide JS

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

Highslide JS

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

Highslide JS

Configuration, symbols
can be added and
configured

Highslide JS

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

Highslide JS

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

Contact Prover