Expertise – Learn about Interlocking Design Automation and Formal Methods 2018-03-05T15:20:44+00:00


Be Inspired and Learn about Interlocking Design Automation and Formal Methods


Demonstration of an Interlocking Design Automation solution

This webinar is a demonstration of a modern Interlocking Design Solution based on Prover Trident


Book an 1:1 Workshop with us!

We offer you the ability to book a 1:1 inspiration workshop. During this workshop we will do the following:

  • Present the demand that is driving the need for change for interlocking design
  • The root causes for why we have a challenging situation today
  • The new future process for Interlocking Design Automation
  • The benefits that this will deliver
  • Give you an overall road map for how you can change your organisation towards a modern solution based on your current situation.
Book a workshop



White Paper – The Prover iLock Process

White Paper - The Prover iLock Process Significant savings with the Prover iLock Process Prover iLock is a tool suite that automates software development of computerized interlocking systems. New CENELEC [...]



ATC, is an integrated signalling system that guarantees the secure movement of trains. ATC integrates various subsystems positioned on-board and wayside. In addition to a full interlocking system, a complete ATC system consists of three subsystems: (i) ATP, (ii) ATO and (iii) ATS.


Automatic Train Operation, or ATO, is an ATC subsystem which performs on-board, non-vital functions normally performed by a train driver, including ensuring a smooth acceleration of the train to the running speed, speed regulation and smoothly stopping the train at the proper position at station platforms or in front of stopping signals. ATO subsystems are primarily located on-board and represent one of the principal components of a driverless system. Additionally, ATO subsystems report vehicle health status to the central control offices.


Automatic Train Protection, or ATP, is an ATC subsystem responsible for the safe operation of a signalling system. It imposes speed limits on trains, both to maintain a safe operating distance between them and to comply with safety and speed requirements. The ATP system is designed to be a fail-safe (vital) system.


Automatic Train Supervision, or ATS, is an ATC subsystem which operates to control trains automatically by means of ATO and ATP, in accordance with the railway timetable. This also involves a CTC system


An electronic beacon or transponder placed between the rails of a railway as part of an Automatic Train Protection system.


Computer Based Interlocking, or CBI, is an Interlocking System where the traditional wired networks of relays are replaced by software logic running on special-purpose fail-safe control hardware. The fact that the logic is implemented by software rather than hard-wired circuitry greatly facilitates the ability to make modifications when needed by reprogramming rather than rewiring.


Communication Based Train Control, or CBTC, is a system under development that will allow for the interchangeability of different technological systems in use on various metro lines. CBTC can be understood as an attempt to create an ERTMS type standard for the mass transit industry.


European Committee for Electrotechnical Standardization.


A Centralized Traffic Control system, or CTC, monitors the status of signalling on a line or network and displays the relevant status information to a central operator, assists in the management of the line or network consistent with the timetable and exercises control to prevent small schedule disturbances from becoming traffic jams. CTC also notifies the operator of ATC equipment failures and of failures in traction power and passenger station support facilities.


Dynamic Railway Information Management System


European Union Agency for Railways.


The European Rail Traffic Management System, or ERTMS, ERTMS was introduced by the EU in 1992 as a means of creating a uniform system of command, control and coordination of rail traffic to allow for ‘‘interoperability’’ throughout EU territory. The ERTMS standard exists at three levels (ERTMS 1, 2 and 3) depending on use, each distinguished by the type of wayside and on-board equipment used and the manner in which this equipment communicates relevant data.


The European Train Control System (ETCS) is a signalling, control and train protection system designed to replace the many incompatible safety systems currently used by European railways, especially on high-speed lines.


European Initiative Linking Interlocking Subsystems.

Formal Verification

To prove automatically with mathematical methods that a system fulfills certain precise requirements


A generic application (GA) is something that can be used as a basis for a number of specific applications. Th GA is specified in sufficient detail to enable interlocking software for specific applications to be automatically generated, formally verified and simulated.


Generic Design Specification. Design principles are formalized in a GDS. It specifies how generated systems shall be designed.


(Global Navigation Satellite System) satellite-based global navigation system, can rely on US GPS (Global Positioning System) or Russian GLONASS (Global Navigation Satellite System) or European Galileo system under development.


Generic Safety Specification. Safety Requirements are formalized in a GSS. It specifies rerquirements that shall be formally verified for every generated system.


Generic Test Specification. Functional requirements are formalized in a Generic Test Specification (GTS). It specifies requirements that shall be checked by simulation for every generated system.


HLL is an expressive formal language well suited as target language for certifiable translators from specification, design and code languages.


High Speed Line, or HSL, refers to railway lines with capacity for speeds in excess of 200 km/h (125 mph).


International Railway Industry Standard.


An interlocking system is responsible for the reliable and safe movement of trains inside a station, through complex junctions and for the length of the line. The interlocking system ensures that train movement is permitted only when a route is available and the switches along this route are safely locked in their position. In all cases the interlocking allocates a track portion or a route to one train at a time, excluding all others.


Light Rail Transit, or LRT, refers to a form of urban rail transit that utilizes equipment and infrastructure that is typically less massive than that used for metro systems, with modern light rail vehicles usually running along the system.


Optimizing Traffic Planner, or OTP, is a traffic management system that permits real time monitoring of the positioning of trains throughout a railway system. OTP optimizes system or network capacity by safely minimizing the time between trains, thereby reducing operating costs. OTP is primarily designed for those markets where railway systems infrastructure is being used to full capacity.


PiSPEC is a specification language that has been designed for interlocking systems specifications. It builds on wellknown concepts that are being taught in engineering classes all over the world.


Positive Train Control: North American freight railway implementation of CBTC.


Reliability, Availability, Maintainability and Safety


Relay Based Interlocking is an interlocking system consisting of a complex circuitry made up of relays in an arrangement of relay logic that ascertain the state or position of each signal appliance


The specific application (SA) is being generated based on the generic application (GA) and specific application configuration data such as track layout, wayside object properties etc.


Shift2Rail will be the first European rail joint technology initiative to seek focused research and innovation (R&I) and market-driven solutions by accelerating the integration of new and advanced technologies into innovative rail product solutions.  Shift2Rail will promote the competitiveness of the European Rail Industry and will meet the changing EU transport needs.


SSI is the brand name of the first generation processor-based interlocking developed in the 1980s by British Rail’s Research Division, GEC-General Signal and Westinghouse Signals Ltd in the UK.


Traffic Management System.


Association of the European Rail Industry.