FAQ
FAQ & Glossary
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 signaling 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 formal system is called complete if every valid formula can be proved in the system.
A Centralized Traffic Control system, or CTC, monitors the status of signaling 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.
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.
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 signaling, 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.
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.
Formal methods are mathematical techniques for the specification, development and verification of software and hardware systems. Learn more about Formal methods here.
A description of a system in a well-defined formal language such as PiSPEC or HLL. Read more about Formal specification here.
Formal verification is a process that uses mathematical models to rigorously prove the correctness and safety of a system’s design, ensuring that it meets all specified requirements without errors. Read more about formal verification here.
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 (GDS) specifies how generated systems shall be designed. Design principles are formalized in a GDS.
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.
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.
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.
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.
High Speed Line, or HSL, refers to railway lines with a capacity for speeds in excess of 200 km/h (125 mph).
IRIS stand for 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.
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.
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.
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.
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 well-known concepts that are being taught in engineering classes all over the world.
Predicate logic or first-order logic uses quantified variables and allows the use of statements that contain predicates and variables.
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.
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.
Propositional logic is the formal logic of the operations AND (conjunction), OR (disjunction), NOT (negation) and IMPLIES (implication).
Positive Train Control (PTC) is the North American freight railway implementation of CBTC.
RAMS stand for Reliability, Availability, Maintainability and Safety.
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.
Program refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program.
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.
Safety property is a property that must be fulfilled by the system in order for the system to be considered safe.
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.
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.
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.
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.
A set of the system states which are represented by all possible combinations of the values of state variables in the system.
As the number of state variables in the system increases, the size of the system state space grows exponentially.
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.
TMS stand for Traffic Management System.
Formal Methods refer to mathematically based techniques and tools for the specification, development, and verification of software and hardware systems. FM helps in designing systems that are error-free and conform to their specifications, particularly critical in industries where safety and reliability are paramount, like the railway signaling and control domain.
Adopting Formal Methods can significantly enhance the reliability, safety, and efficiency of complex systems within your organization. Benefits include reduced costs associated with testing, bug fixing, and maintenance, as well as shorter development cycles and faster implementation times. Formal Methods provides a robust framework for managing complexity and ensuring system integrity.
The “Prestudy: Formal Methods Business Case” is a service offered by Prover designed to assess your organization’s readiness to adopt Formal Methods. It includes evaluating your current processes, data structure, and requirements clarity, and provides a detailed plan on how to start implementing FM, along with understanding the potential savings and business case.
This service is ideal for management teams at Infrastructure Managers (IMs) who are curious about Formal Methods but unsure if it’s suitable for their operations. It’s particularly beneficial for decision-makers seeking to understand the potential impact and benefits of FM on their systems and processes.
The project kicks off with an initial meeting to explain the process, gather input, and answer questions. Prover’s team then conducts a two-week in-depth analysis, followed by a follow-up meeting where a comprehensive report and action plan are presented, detailing the steps towards Formal Methods integration and the associated benefits.
You will receive a written report with a clear plan and steps needed to start with Formal Methods, an executive summary for quick insights, a presentation of the findings, and supporting material to present the business case for Formal Methods within your organization.
Getting started is easy. Simply fill out the form on our landing page, or reach out to us via the provided contact information. Our team will get in touch to discuss your needs and how we can help you embark on your Formal Methods journey.
Phone: +46 (0)8 617 68 00
E-mail: info@prover.com
Model-Based Tendering is a process that uses digital twins and simulations to validate project requirements before the tendering phase begins. This approach ensures requirements are realistic, achievable, and free from contradictions. The purpose is to decrease risks in projects.
Digital Twins play a crucial role by providing a virtual prototype of the proposed project, allowing for detailed testing and validation of requirements. They offer a platform for stakeholder feedback and ensure the project’s feasibility before any physical work starts.
Yes, by identifying and resolving conflicts and unrealistic requirements early on, Model-Based Tendering can significantly reduce the need for costly changes during later project stages, leading to more predictable and controlled project costs.
It allows stakeholders to visualize and interact with a model of the project early in the process, ensuring their requirements and concerns are addressed before the project is finalized. This early engagement helps to align expectations and increase satisfaction.
While especially beneficial for complex projects where the integration of new systems with existing ones is critical, Model-Based Tendering can be adapted to suit a wide range of projects by ensuring that project requirements are clear, validated, and achievable from the outset.
It streamlines the tender process by providing clearer, validated project specifications, reducing the likelihood of ambiguous requirements. This leads to more accurate bids from contractors and a smoother selection process.
The first step is to assess the current tendering process and identify areas where digital twins and simulations can add value. Then, develop a strategy for integrating these technologies into the tendering process, including training for key personnel on how to use and interpret digital twins effectively.
A Digital Twin is a virtual model of a real-world railway signaling system. It’s used to simulate, analyze, and optimize the system in a virtual environment, helping to predict and solve potential problems before they occur in the real world.
It allows for detailed analysis and testing of the signaling system under various conditions, identifying potential safety issues and vulnerabilities that can then be addressed to prevent accidents and improve reliability.
Digital Twins can detect complex issues like subtle software bugs, design flaws, and unforeseen interactions between system components that might be missed by traditional testing and manual inspections. They do so by using powerful methods such as formal verification, simulation and visualization.
If your system suffers from frequent maintenance issues, safety concerns, or if you’re planning an upgrade or expansion, Digital Twin technology can provide insights and foresight into potential improvements and optimizations.
You’ll need to provide detailed system specifications, operational data, and any existing design or infrastructure information. This will help us create an accurate Digital Twin of your signaling system.
The setup time can vary depending on the complexity of the system, but typically, initial results and insights can be obtained within a few weeks to a few months after starting the process.
We provide detailed reports on identified issues, along with recommendations for rectification. We can also offer ongoing support and consultation for implementing these changes and optimizing your system.
Yes, we employ stringent data security measures to ensure all your data remains confidential and secure throughout the analysis process.
While there’s an upfront investment, the long-term benefits include reduced maintenance costs, fewer system downtimes, and prevention of costly accidents, making it a cost-effective solution for enhancing system safety and efficiency.
Yes, it’s designed to be compatible and can often be integrated with existing management systems to enhance overall operational insights and decision-making.
We recommend conducting a comprehensive analysis annually or bi-annually, and also whenever major system changes or upgrades are planned, to ensure ongoing safety and performance optimization.
+46 (0)8 617 68 00