(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 & 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?2024-03-05T10:09:02+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?2024-03-05T10:10:10+01:00

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.

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.

What are Formal Methods (FM)?2024-03-05T09:36:29+01:00

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.

Why should my organization consider adopting Formal Methods?2024-03-05T09:36:21+01:00

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.

What is the “Prestudy: Formal Methods Business Case”?2024-03-05T09:20:43+01:00

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.

Who should consider the prestudy?2024-03-05T09:22:13+01:00

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.

What does the project process involve?2024-03-05T09:24:38+01:00

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.

What deliverables can we expect from the prestudy?2024-03-05T09:26:12+01:00

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.

How can we get started with the prestudy?2024-03-05T09:29:14+01:00

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

What is Model-Based Tendering?2024-03-05T09:51:58+01:00

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.

How does Digital Twin technology fit into Model-Based Tendering?2024-03-05T09:40:26+01:00

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.

Can Model-Based Tendering reduce project costs?2024-03-05T09:42:07+01:00

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.

How does Model-Based Tendering benefit stakeholders?2024-03-05T09:45:19+01:00

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.

Is Model-Based Tendering suitable for all types of projects?2024-03-05T09:47:00+01:00

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.

How does Model-Based Tendering impact the tender process?2024-03-05T09:57:24+01:00

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.

What are the first steps to implementing Model-Based Tendering in an organization?2024-03-05T09:49:03+01:00

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.

What is a Digital Twin?2024-03-05T10:04:52+01:00

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.

How does Digital Twin technology help in improving railway signaling safety?2024-03-05T10:06:36+01:00

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.

What kind of issues can Digital Twins detect that traditional methods cannot?2024-03-05T10:08:14+01:00

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.

How can I know if my current railway signaling system can benefit from Digital Twin technology?2024-03-05T10:11:19+01:00

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.

What is required to start using your Digital Twin technology?2024-03-05T10:12:12+01:00

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.

How long does it take to set up a Digital Twin and see results?2024-03-05T10:13:27+01:00

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.

What support do you offer after identifying signaling issues?2024-03-05T10:14:21+01:00

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.

Is the data secure when using Digital Twin technology?2024-03-05T10:19:15+01:00

Yes, we employ stringent data security measures to ensure all your data remains confidential and secure throughout the analysis process.

How cost-effective is implementing Digital Twin technology?2024-03-05T10:34:25+01:00

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.

Can Digital Twin technology be integrated with existing railway infrastructure management systems?2024-03-05T10:35:42+01:00

Yes, it’s designed to be compatible and can often be integrated with existing management systems to enhance overall operational insights and decision-making.

How often should a Digital Twin analysis be performed on a railway signaling system?2024-03-05T10:36:36+01:00

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.

Go to Top