Expertise
WEBINARS
Webinar – Building a safety case for rail control software with Formal Verification
Learn how formal verification, implemented with a pre-qualified T2 SIL4 tool, Prover Certifier, can be used in a CENELEC EN50128 compliant process.
Recorded Webinar – Modeling rail control systems with digital twins
In this webinar, we look at digital twins can be used in modeling rail control systems and present a case from Stockholm Metro.
Recorded Webinar – Get in control of your rail control system
Learn more about how to get on top of your signaling projects using a digital twin and signaling design automation.
Recorded Webinar – How to guarantee safety of rail control systems with formal verification
In this webinar, you will learn how formal verification, a technique that gives 100 % coverage and can be fully automated, can guarantee safety of rail control systems.
Recorded Webinar – Developing rail control software based on digital twins and signaling design automation
This webinar covers how to overcome challenges in the delivery of rail control software using a formal development process we call Signaling Design Automation.
Recorded Webinar – Establishing safety with Formal Verification
Safety is critical for the railway industry. We believe the method that should be used for safety assurance is Formal Verification. Join us in a webinar on this subject.
WHITE PAPERS
How to Develop Rail Control Software with Signaling Design Automation and Digital Twins
In this guide, we will run through the basics of how you can use SDA and Digital Twins to develop rail control software.
Developing Specifications with Digital Twins
In this guide, we focus on how the specification phase of rail control projects can be improved by using formal methods and Digital Twins.
Successful rail control projects with Signaling Design Automation
In this guide, we walk you through our formula for successful rail control projects, called Signaling Design Automation.
Engineering safe rail control with Formal Verification
In this white paper we discuss why we believe Formal Verification is the best method for verifying safety and should be used when engineering safe rail control systems.
Safety Verification Methods for Rail Control Software
In this article we give an overview of the safety verification practices commonly used in rail control projects in The United States, Sweden and France.
Signal Modernization at Stockholm Metro
In this white paper we will take a closer look at two modernization projects of the Stockholm Metro. One based on legacy relay interlocking and the other utilizing modern computerized interlockings.
Automated verification and validation of signaling systems in PTC and CBTC environments
In this document, we will show how you can avoid certain problems as long as proper care is taken from the very start of the project.
The Process for Interlocking Design Automation
In this document, we will present a process that gives significant benefits for both the supplier and the infrastructure manager during a project.
The Business Case for Interlocking Design Automation
This document aims to help infrastructure- vendors and managers developing rail control systems to create a compelling business case for investing in a modern Interlocking Design Automation process.
VIDEOS
HLL Forum – The community for those who use HLL
The HLL Forum is the community for us who use the formal specification language HLL, and believe it is a good language for formal methods. As it has started to become a de facto standard, we want to make sure that the language develops in a controlled way to meet the demands of the future.
GLOSSARY
ATC
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.
ATO
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.
ATP
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.
ATS
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
Balise
An electronic beacon or transponder placed between the rails of a railway as part of an Automatic Train Protection system.
CBI
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.
CBTC
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.
CENELEC
European Committee for Electrotechnical Standardization.
Completeness
A formal system is called complete if every valid formula can be proved in the system.
CTC
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.
Domain-Specific Language/DSL
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.
DRIMS
Dynamic Railway Information Management System
ERA
European Union Agency for Railways.
ERTMS
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.
ETCS
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.
EULYNX
European Initiative Linking Interlocking Subsystems.
Finite state machine/FSM
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
Mathematical techniques for the specification, development and verification of software and hardware systems.
Formal specification
A description of a system in a well-defined formal language such as PiSPEC or HLL.
Formal Verification
To prove automatically with mathematical methods that a system fulfills certain precise requirements
GA
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.
GDS
Generic Design Specification. Design principles are formalized in a GDS. It specifies how generated systems shall be designed.
GNSS
(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.
GSS
Generic Safety Specification. Safety Requirements are formalized in a GSS. It specifies rerquirements that shall be formally verified for every generated system.
GTS
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
HLL is an expressive formal language well suited as target language for certifiable translators from specification, design and code languages.
HSL
High Speed Line, or HSL, refers to railway lines with capacity for speeds in excess of 200 km/h (125 mph).
IRIS
International Railway Industry Standard.
IXL
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.
LRT
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.
Model-based development
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.
Model checking
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.
Model transformation
A program that take models as input and generate the target models as output and meanwhile keep 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.
OTP
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
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.
Predicate logic
Predicate logic or first-order logic uses quantified variables and allows the use of statements that contain predicates and variables.
Process calculus
A tool for 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
A logical formula associated to 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
The formal logic of the operations AND (conjuction), OR (disjunction), NOT (negation) and IMPLIES (implication).
PTC
Positive Train Control: North American freight railway implementation of CBTC.
RAMS
Reliability, Availability, Maintainability and Safety
RBI
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
Refinement
Program refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program.
SA
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
A property that must be fulfilled by the system in order for the system to be considered safe.
SAT
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 to the property.
Shift2Rail
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.
Soundness
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
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.
State space
A set of the system states which are represented by all possible combinations of the values of state variables in the system.
State space explosion
As the number of state variables in the system increases, the size of the system state space grows exponentially.
Theorem proving
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
Traffic Management System.
UNIFE
Association of the European Rail Industry.