Prover Technology - Railway Control and Signalling Systems

Prover Technology is a world-leading provider of software products for development and V&V of railway control and signalling systems, such as CBTC, ERTMS and interlocking systems. By utilizing Prover Technology’s products, customers reduce development costs and see their time-to-market measures shrink significantly. Safety evidence for CENELEC SIL 4 certification is automatically produced by the push of a button making code review and safety testing unnecessary.

• Prover iLock automates development of railway control and signalling systems with unparalled efficiency.
• Prover Certifier is the only product on the market that can automatically create complete safety evidence for CENELEC EN50128 SIL 4 certification based on formal verification.
• Prover Extractor offers development and V&V of relay-based interlocking systems.

Customers are leading signalling system suppliers and infrastructure managers and include:

• Ansaldo STS
• Bombardier Transportation
• Canadian Pacific Railway
• General Electric
• Invensys Rail
• New York City Transit
• Norwegian National Rail
• Paris Metro (RATP)
• Stockholm Metro (SL)
• Swedish National Rail
• Thales RSS

Development and V&V of railway control systems

With Prover iLock, a new system is developed, simulated and verified in les than one day. Using world-leading methods for automatically establishing that systems are safe and fully functional, V&V procedures are made highly automatic. As the generic application is reused, savings increase with a higher number of specific applications being developed.

The Prover iLock product suite integrates formal verification with other push-button tools for highly automated development of computerised interlocking systems including:

• Generation of design, test cases and safety requirements
• Generation of software code for the target platform
• Formal  verification of all safety requirements with 100% coverage
• Functional testing of all test cases, co-simulated with environment models
• Generation of documentation
• Generation of test cases for factory testing (FAT), hardware-in-the-loop testing (HIL) and commissioning (SAT) testing

The Prover iLock process is based on a generic application, defined in the formal specification language PiSPEC, which is reused for multiple specific applications.

Safety evidence for CENELEC SIL 4 certification

Prover Certifier provides automatic production of complete safety evidence for CENELEC EN50128 SIL 4 certification. Replacing time-consuming and incomplete safety testing and manual reviews with formal verification, Prover Certifier provides 100% coverage in a fraction of the time required for traditional V&V activities. Prover Certifier is used for ERTMS, CBTC and interlocking systems by different system suppliers and supports several development flows.

Software tools for development of relay-based systems

Prover Extractor checks and extracts information from relay circuit schematics for relay-based interlocking (RBI) systems. Design consistency and conformance to design guidelines can be checked and extracted information can be used for formal verification or simulation of the system. It also offers a relay database for efficient maintenance of relays.

Services for safety assessment and development

The company provides services for training, safety assessment of railway control and signalling systems, and formal specification of railway signalling principles and requirements.