(function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start': new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0], j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.data-privacy-src= 'https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f); })(window,document,'script','dataLayer','GTM-KZ3W38S');
Frequenty Asked Questions2023-04-26T16:25:43+01:00

FAQ

FAQ & Glossary

What is ATC?2023-04-13T12:36:12+01:00

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.

What is ATO?2023-04-13T12:36:33+01:00

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.

What is ATP?2023-04-13T12:36:54+01:00

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.

What is ATS?2023-04-13T12:37:18+01:00

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

What is Balise?2023-04-13T12:37:45+01:00

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

What is CBI?2023-04-13T12:38:02+01:00

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.

What is CBTC?2023-04-13T12:38:22+01:00

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.

What does CENELEC stand for?2023-04-13T12:38:38+01:00

European Committee for Electrotechnical Standardization.

What does Completeness mean?2023-04-13T12:38:55+01:00

A formal system is called complete if every valid formula can be proved in the system.

What is CTC?2023-04-13T12:39:10+01:00

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.

What is Domain-Specific Language / DSL?2023-04-13T12:39:34+01:00

Domain-Specific Language / DSL is a programming language for a particular application domain. This is in contrast to a general-purpose language (GPL), which is broadly applicable across domains. There are a wide variety of DSLs, ranging from widely used languages for common domains, such as HTML for web pages, to the railway specific application languages RailML which is used for data exchange between objects in railway systems. PiSPEC is a DSL for interlocking system specifications.

What does DRIMS stand for?2023-04-13T12:39:56+01:00

Dynamic Railway Information Management System.

What does ERA stand for?2023-04-13T12:40:12+01:00

European Union Agency for Railways.

What is ERTMS?2023-04-13T12:40:29+01:00

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.

What is ETCS?2023-04-13T12:46:20+01:00

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.

What does EULYNX stand for?2023-04-13T12:46:35+01:00

European Initiative Linking Interlocking Subsystems.

What is Finite state machine (FSM)?2023-04-13T12:46:52+01:00

Finite state machine (FSM) is an abstract machine that can be in exactly one of a finite number of states at any given time and can change from one state to another in response to some external inputs. The change from one state to another is called a transition.

What are formal methods?2023-04-13T12:47:19+01:00

Formal methods are mathematical techniques for the specification, development and verification of software and hardware systems.

What is formal specification?2023-04-13T12:48:23+01:00

A description of a system in a well-defined formal language such as PiSPEC or HLL. Read more about Formal specification here.

What is formal verification?2023-04-13T12:49:27+01:00

Formal verification is a way to prove that a system fulfills certain precise requirements with mathematical methods. Read more about formal verification here.

What is generic application (GA)?2023-04-13T12:49:44+01:00

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.

What is Generic Design Specification (GDS)?2023-04-13T12:50:05+01:00

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

What is Global Navigation Satellite System (GNSS)?2023-04-13T12:50:27+01:00

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

What is GSS?2023-04-13T12:50:49+01:00

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

What is GTS?2023-04-13T12:51:04+01:00

GTS stand for 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.

What is High Level Language (HLL)?2023-04-13T12:52:06+01:00

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

What is High Speed Line (HSL)?2023-04-13T12:54:14+01:00

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

What does IRIS stand for?2023-04-13T12:54:41+01:00

IRIS stand for International Railway Industry Standard.

What is IXL?2023-04-13T12:55:23+01:00

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.

What is Light Rail Transit (LRT)?2023-04-13T12:55:40+01:00

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.

What is Model-based development?2023-04-13T12:55:55+01:00

A software development methodology that focuses on creating and exploiting domain models, which are conceptual models of all the topics related to a specific problem. Hence, it highlights and aims at abstract representations of the knowledge and activities that govern a particular application domain, rather than the computing (i.e. algorithmic) concepts.

What is Model checking?2023-04-13T12:56:12+01:00

A method for formally verifying finite-state concurrent systems. Specifications about the system are expressed as temporal logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not.

What is model transformation?2023-04-13T12:56:36+01:00

A program that takes models as input and generates the target models as output and meanwhile keeps the information consistent. The aim of using a model transformation is to save effort and reduce errors by automating the building and modification of models where possible.

What is an Optimizing Traffic Planner (OTP)?2023-04-13T12:57:10+01:00

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.

What is PiSPEC?2023-04-13T13:07:08+01:00

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

What is predicate logic?2023-04-13T13:07:08+01:00

Predicate logic or first-order logic uses quantified variables and allows the use of statements that contain predicates and variables.

What is process calculus?2023-04-13T13:07:08+01:00

Process calculus is a tool for the description of interactions, communications, and synchronizations between a collection of independent agents or processes. They also provide algebraic laws that allow process descriptions to be manipulated and analyzed and permit formal reasoning about equivalences between processes.

What is a proof obligation?2023-04-13T13:07:08+01:00

Proof obligation is a logical formula associated with a correctness claim for a given verification property. The formula is valid if and only if the property holds in all interpretations. The correctness of the property under verification is “delegated” to proving the correctness of this formula.

What is propositional logic?2023-04-13T13:07:07+01:00

Propositional logic is the formal logic of the operations AND (conjunction), OR (disjunction), NOT (negation) and IMPLIES (implication).

What is Positive Train Control (PTC)?2023-04-13T13:07:07+01:00

Positive Train Control (PTC) is the North American freight railway implementation of CBTC.

What does RAMS stand for?2023-04-13T13:07:07+01:00

RAMS stand for Reliability, Availability, Maintainability and Safety.

What is Relay Based Interlocking (RBI)?2023-04-13T13:07:07+01:00

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

What is program refinement?2023-04-13T13:07:06+01:00

Program refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program.

What is a specific application (SA)?2023-04-13T13:07:06+01:00

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.

What is safety property?2023-04-13T13:07:06+01:00

Safety property is a property that must be fulfilled by the system in order for the system to be considered safe.

What is SAT?2023-04-13T13:07:06+01:00

The Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. SAT techniques can be used to prove or disprove properties: if the negation of a property cannot be satisfied, then the property is valid. If the negation of a property is satisfied by a certain interpretation, then this interpretation is a counterexample of the property.

What is Shift2Rail?2023-04-13T13:07:05+01:00

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.

What is Soundness?2023-04-13T13:07:05+01:00

A formal system is sound if and only if every formula that can be proved in the system is valid with respect to the semantics of the system.

What is SSI?2023-04-13T13:07:05+01:00

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.

What is state space?2023-04-13T13:07:05+01:00

A set of the system states which are represented by all possible combinations of the values of state variables in the system.

What is state space explosion?2023-04-13T13:07:04+01:00

As the number of state variables in the system increases, the size of the system state space grows exponentially.

What is theorem proving?2023-04-13T13:07:04+01:00

A subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

What does TMS stand for?2023-04-13T13:07:04+01:00

TMS stand for Traffic Management System.

What is UNIFE?2023-04-13T13:07:03+01:00

Association of the European Rail Industry.

Go to Top