Some systems are constructed by instantiating some generic design patterns on a collection of items (i.e. data). In the railway industry, the most widespread use of this mechanism is found for IXL, and to a lesser extend track-side ERTMS and CBTC systems.

While the overall structure of the S3 solutions dedicated to these kind of systems is not very different from that of the “standard” solutions described in the post about S3 workflow, they still admit some specificities. This section follows the structure of the aforementioned post and address these specificities.

This section will focus on IXL systems, but most of it could be adapted to other instantiated systems.

Note

This post is the third of a serie of four. You may also be interested by the two previous posts:

An IXL 1 is a system commanding and controlling the signals and switches (or points) of a railway track layout, ensuring safe train operations. The first IXL systems, arising around 1850, where mechanical devices. Next, in the 30s, these systems became mainly implemented using electro-mechanical devices, the RBI. Since the 80s, these systems tends to be replaced by computers running software controlling the track-side devices, the CBI.

The S3 model checking solutions have been shown to be particularly efficient in proving the safety of CBI systems 2.

For practical reasons, in the examples of this section the track layout is subdivided in small linear parts, called Blocks, that shall not overlap on track-circuits boundaries, and which stops at signals, derailers, and switches cores (i.e. a switch contains three such linear blocks).

Interlocking Development Workflows¶

The vital code of a CBI is typically obtained through a process known as instantiation 3. In such a process, the signaling principles are captured by the users to produce the Generic Design in some suitable language. This design contains a set of generic code snippets that an IXL system shall execute for each object of a given category, such as signals, switches, routes,… Each of these generic snippets is given in a parametrized form allowing to specialize it for the object to which it applies. For example, the generic code for a route will most probably be parametrized with the list of switches contained in the route. The generic design is thus specific to a set of signaling principles, but independent of a particular track layout.

To instantiate the IXL system for a particular track layout, the geographical data representing this particular station topology is first processed by a data-preparation tool and gathered in some sort of database. This database contains the population of objects of the given station (e.g. signals, routes, switches,… ) and the relations between these elements ( starting signal of a route, switches contained in a route,… ). An instantiation tool is then used to create “copies” of the elements of the generic design, called instances, for each object of the given station 4. Each instance is specialized by receiving the specific parameters values for the object to which it applies. The instantiated system is not necessarily produced as “code” in the common sense (a software in some known programming language), it can take many forms: boolean equations, ladder diagrams, automatons, or even mere data-tables. Such an instantiated system can then be interpreted by a generic software engine, or used as a design to generate the actual code.

Numerous alternatives of this process exists, three of the most common ones are depicted, in an overly simplified way, in the following IXL development figure. In the first alternative, the instantiation tool creates an instantiated design, which is later processed by a code generator, or some sort of compiler, to produce the actual instantiated vital code. In the second alternative, the instantiation tool directly creates the instantiated vital code suitable for execution on the IXL hardware platform (the copy of the obtained code is just an artificial way of obtaining a unified interface of the different process alternatives with the S3 workflow presented in the following sections, see in particular section Specific S3 Workflows). The last alternative process is an extension of the second alternative, used for certification purposes, in which two independent and diversified instantiation tools produce two independent instantiated implementations. They are then either loaded on an IXL hardware platform which runs both and contains some sort of output comparison or voting device, or merely compared to show that they are identical.

Alternative Interlocking Development Processes

The first alternative will be used in the following sections to illustrate the use of the S3 workflow. The usages for the other workflows are fairly similar, but some specificities are discussed in section Specific S3 Workflows.

Generic Safety Specification¶

The major specificity of an S3 solution for IXL systems is not the architecture of the solution, but rather the safety specification (i.e. the safety properties and the environment model) against which the system has to be verified (see preliminary post).

As an introductory remark, it is important to understand that, as the system is instantiated for a given station track layout, the formal safety verification performed on this system will only address the safety on this particular track layout. It is not a generic proof that the design is safe for every station track layout 5. In particular, the proof will have to be conducted each time a system is instantiated with a new track layout.

Having to prove every instance is however not a problem because for generic systems instantiated by data, such as an IXL instantiated for a specific station track layout, the safety specification, but also the needed induction strengthening lemmas, are usually also generic, and can be automatically instantiated using the same data. Developing and verifying the GSS is thus done only once, and proving that an instance on a specific station track layout verifies the instantiated on this same track layout is completely automated in the S3 solution.

Support for Genericity¶

The genericity of the safety specification is supported by three central elements of the HLL language (see Modeling Languages section in the previous post):

sorts, a set of types representing a hierarchical enumerated population. Sorts are used to represent objects. First the object classes are declared (e.g. signals, switches, routes,… ) and used to develop the GSS. Later, during the instantiation process, these classes are populated with the object instances present on the track layout of the specific station.
functions over objects represented as sorts (e.g. start_signal(route)), and especially predicates, i.e. boolean functions over sorts. Predicates are used to represent relations between objects (e.g. reachable(block1,block2), contains(route,block),… ), to access variables of the design, or to provide insulation layers (see next paragraph).
quantification, universal (\(\forall\), ALL) and existential (\(\exists\), SOME) quantification over finite sets, such as sorts. Quantifications are used to “apply” an expression to every member of the finite set over which it ranges. For example the fact that every block belonging to a given route is free can be expressed as:
```
ALL b:BLOCKS (contains(route,b) -> free(b))
```
where ALL is the universal quantifier, b:BLOCKS indicates that b shall range on every instances of the BLOCKS sort, and -> is the implication operator.

When developing a GSS, different kinds of predicates are usually considered:

topological predicates, these low-level predicates encode the topology of the track layout, such as the ordering of blocks, the location of signals on blocks, the location of switches, the objects contained in a route, … They are only declared in the GSS. Their precise definition is provided later during the instantiation process by translation of the specific station track layout.
integration predicates, these low-level predicates are used to access boolean inputs, outputs, and local variables of the design, and to associate them with particular object instances (e.g. track-circuits occupancy sensors, switches position sensors, signals actuators, …). These predicates are only declared in the GSS. They are also defined later, usually by a solution-specific tool expanding the names of object instances into a string pattern capturing the variable naming convention used in the design.
insulation predicates, this predicate layer can be used to rename the low-level predicates in order to enforce independence of the GSS from the naming conventions used in the design.
intermediate helper predicates, these predicates are defined using sorts, quantification, and lower level predicates. They are used as helpers in the formalization of the environment constraints and the safety properties. They usually convey higher level relations between objects such as reachability, incompatibility, statuses, …

Instantiation of the Generic Safety Specification¶

As explained in the previous section, sorts, topological predicates, and integration predicates are first declared and used to express generically the safety properties and environment constraints. Later, when analyzing a specific track layout, the sorts are populated with the actual object instances on the track, the low-level topological predicates are initialized with the relations encoding the track layout, and the integration predicates are initialized with the code variables mappings. Through the evaluation of quantifiers and higher-level predicates performed during expansion (see Uncertified S3 Workflow section in previous post), the GSS applied to this description of the track layout becomes automatically instantiated for this specific layout, and can thus be checked on the given CBI vital code.

Levels of Generic Safety Specifications¶

As for the general case (see Safety Specification section), several levels of GSS exist. Schematically, these levels can be represented by different layers in a pyramid, as shown in the following figure.

Safety Specification Pyramid

The pyramid is capped with the safety hazards identified by the hazard analysis of the system. For an IXL, the core hazards are the derailment of a train, and the collision of a train with another train or with an obstacle (workers on the track, vehicles or pedestrians on a level crossing, …). Additional hazards are usually needed to cover specific signaling principles, and to address the connection of the IXL system with other systems such as a neighboring IXL or a CBTC system.

The layers underneath the hazards cap represent sets of safety properties that, once proved, are sufficient to insure that the system prevents the identified hazards to take place. The part of the pyramid that is below a given layer, including lower layers, down to the base, are the induction enforcing lemmas required to prove the safety properties of this given layer.

The upper layers are characterized by a low number of safety properties, fairly simple to formalize, and unambiguously implying the safety of the system. Moreover, these properties are somewhat only loosely dependent on the specific system design principles, leading to some independence between the safety properties and the signaling principles. All in all, they are simple to review for correctness and completeness. However, the drawback of the safety properties of these upper layers is that they require more induction strengthening lemmas, more power from the analysis engine, but also a complex environment model describing how a train can move, when it can cross a signal, when it can reverse direction, when a switch can move, …

Conversely, the lower layers of the pyramid contains a larger number of properties. They usually require less lemmas, and are simpler to prove. However, it is difficult to show that the set of properties is complete and sufficient to ensure the overall safety of the IXL system. They are also more complex to formalize and thus difficult to review for correctness. Also, being strongly dependent on the design and signaling principles, changes in the design tend to have a strong impact on these safety properties.

The next paragraphs briefly describes different layers of the core safety specifications that are typically used in S3 formal safety verification solutions for IXL systems.

Train Oriented Safety Specification¶

At the highest level of the pyramid, the Train Oriented Safety Specification addresses the safety hazards in a straightforward manner. Taking the point of view of a given train, the safety properties express directly that the train will not collide with another train or with an obstacle, and that it will not pass over an apparatus that would make it derail (e.g. an ill-positioned switch or derailer). This approach gives a one-to-one correspondence between the safety properties and the safety hazards, making it trivial to both formalize and review the safety properties. As stated in the previous paragraphs, apart from the high number of required lemmas and needed proof power, the major difficulty lies in the complexity of the environment model. For these properties, the environment model needs to specify accurately the possible movements of trains, and in particular to trace trains individually (e.g. to prevent an artificial collision between a train and itself).

SxH Safety Specification¶

The S×H Safety Specification is the result of a methodology to derive a safety specification at a sufficiently high level to retain the advantages in term of ease and clarity of formalization and review, while maintaining the environment model at a reasonable level of complexity (e.g. not considering individual trains, but rather only the presence of a train on a track element).

Signals are the central protection elements of a railway IXL. They are supposed to open (i.e. show a proceed aspect) when and only when they are able to insure a safe path to a train up to the next signal in the same direction. A restricted form of opening, under the responsibility of the driver is also possible in some circumstances (e.g. shunting, incomplete protection, …). Trains are supposed to stop at closed signals, except in a number of well defined situations (e.g. approach-locking, overlap-zones, slipping of parked trains, …).

Given this pivotal role of signals, the Hazard-Zone of a train (resp. a signal) is defined as the part of the track that is reachable in front of the train given its movement direction (resp. in front of the signal given its direction), up to the next signal in the same direction, plus its potential overlap zone. The reachability relation depends on the physical state of the track apparatuses at the given time 6, following the positions of switches, and stopping on ill-positioned switches and active derailers. Examples of hazard-zones from a given train position for different switches positions are illustrated in the hazard zones figure.

The S×H methodology is based on the composition of Situations, an enumeration of possible signal states and train positions and movements, with Hazards reachable from the train or the signal in its hazard-zone.

The situations to consider are the following (see the situation figure for an illustration of the various situations together with their hazard-zones):

a closed and passable signal;
an open signal;
a closed and approachable signal;
a train on a path with a given position and movement direction;
a train slipping on an overlap zone.

where a signal is considered passable if a train was approaching the signal when it closed, and doesn’t have the time to stop. This concepts is usually managed by the IXL system through the combination of an approach-zone and an approach-timer 7. The timer is triggered when the signal closes while a train is on the zone, and the signal is considered approachable until the timer elapses.

Hazard-zones

Situations (w.r.t. signal A)

The S0 situation cannot lead to an accident in the hazard-zone of the signal because a potential train upstream of the signal will have time to stop in front of it. Its hazard-zone is thus empty. For the S1 and S2 situations, the hazard-zone is that of the signal, and for S3 and S4 the hazard-zone is that of the train.

The S1 situation cannot lead to an accident unless a train is present upstream of the signal and before the previous signal in the same direction. This could be added as a prerequisite of the situation if required, effectively splitting the situation in two cases, one without a train for which the hazard-zone is empty, and one with a train for which the hazard-zone is that of the signal. However, it is usually forbidden, or at least suspicious, to open a signal leading to a hazard even if there is no train in front of this signal. This situation is thus usually kept as stated here.

The list of hazards is derived from the top-level safety hazards by considering what could lead to this top-level hazard in the hazard-zone of a given situation. It is of course of ultimate importance that this list is complete, which shall be ensured by a careful review from peers and from the certification authority.

An informative list of the hazards to be considered in the hazard-zones of the situations is given below, but has typically to be amended for the considered signaling principles:

a badly positioned switch is in the hazard-zone

\(\Rightarrow\)may lead to a derailment
a badly positioned derailer is in the hazard-zone

\(\Rightarrow\)may lead to a derailment
a non-protected level crossing is in the hazard-zone

\(\Rightarrow\)may lead to a collision with a vehicle or a pedestrian
a train in the same direction as the situation is in the hazard-zone (different from the train involved in the situation)

\(\Rightarrow\)may lead to a catch-up collision
a block in the hazard-zone is reachable from a facing open signal (facing w.r.t. the direction of the situation)

\(\Rightarrow\)may lead to a frontal collision
a block in the hazard-zone is part of a switch-fouling point, and another block of this fouling-point is reachable from an open signal

\(\Rightarrow\)may lead to a flank collision
a diverging switch is in the hazard-zone and full speed is allowed

\(\Rightarrow\)may lead to an over-speed derailment
a temporary protection zone (e.g. a working zone) is in the hazard-zone

\(\Rightarrow\)may lead to a collision with a protected person or object (e.g. a worker)

where the reachability relation is the same as the one used when defining the hazard-zones.

In the S×H methodology, the safety properties are obtained by composing all the situations (except S0) with all the hazards.

Signaling Principles Based Safety Specification¶

A classical way of deriving the safety specification is to show the conformance of the system with the signaling and design principles, i.e. its requirements. This approach doesn’t address directly the safety of the system, but instead relies on the safety analysis performed when designing the signaling principles. Using such a safety specification, the system is thus shown to comply with its requirements, but, if an error in the requirements fails to insure safety of the overall system, it will not be detected by the formal verification solution.

Another problem of this methodology is that the signaling principles contains the complete system requirements. The part that is not safety specific (i.e. related to functionality or availability), is usually much larger and difficult to prove. Even when the safety specification tries to focus only on the safety part of the requirements, the two parts are usually tangled in such a way that it is difficult to separate them in a convincing way.

All in all, a Signaling Principles Based Safety Specification is rather low-level and does not fit fully in the safety specification pyramid because it is not directly driven by the safety hazards. There may be some holes in the considered layer (if there are safety-critical errors in the requirements), and it can also address more than just safety. Furthermore, the set of properties are tightly bound to the design principles, such that any changes in the design has an impact on the safety properties.

Uncertified S3 Workflow for Interlocking Systems¶

An uncertified S3 workflow for IXL systems is very similar to the generic workflow seen in Uncertified S3 Workflow section of previous post. The main difference is the need for a tool to translate the topology of a specific station track layout into populations of object instances (given as sorts population), and low-level topological predicate definitions (see section Generic Safety Specification). The HLL syntax for these is very simple and usually such translators are quite straightforward, just rewriting some kind of database to the HLL format.

Concatenating the result of this translation and the GSS produces the Instantiated Safety Specification. With sorts being populated, and low-level predicates defined in such a way as to describe the specific station topology, the whole GSS becomes specialized for this particular station.

A translator from the instantiated design language to HLL is then used to translate the instantiated design into a (usually) bit-precise HLL model preserving its execution semantics. This model is then concatenated to the instantiated safety specification. The use of the integration predicates in the GSS, and the definition of these as mappings from sort object instances to variables of the design translation, automatically connects the instantiated safety specification with the instantiated IXL design model. Thus, the resulting HLL file contains the instantiated system and safety specification ready for analysis.

The rest of the solution is identical to the generic solution (see Uncertified S3 Workflow section of previous post. The overall uncertified workflow synoptic for systems is given in the following figure.

Uncertified S3 Workflow Synoptic for Interlocking Systems

The induction strengthening lemmas constructed by applying the iterative methodology described in preliminary post are also written using the HLL language. They are inferred from the investigation of step-counter-examples generated by the analyses of instantiated safety properties on an instantiated system (usually a test system). They are thus found in an instantiated form, and must be generalized to be expressed in a generic way similarly to safety properties, using sorts, predicates, and quantification. However, contrarily to these, they usually also need to refer to internal memories of the design.

Certifiable S3 Workflow for Interlocking Systems¶

Once the GSS has been validated, the IXL system has been corrected from any safety-related bugs, the lemmas have been developed, and all safety properties proved, it is time to address the problem of the confidence that can be granted to the formal safety verification solution, and the way to reach an EN-50128 certification for a complete IXL development process using this solution. This problem is addressed using the same mechanisms used in the generic solution described in Certifiable S3 Workflow section of previous post. The overall solution synoptic for systems, assembling the different protection mechanisms, is presented in the following figure.

Complete Solution Synoptic for Interlocking Systems

The main specificity is in the protection of the safety verification workflow, which integrates a diversification of the topology translation to protect it together with the expansion of the overall system including the instantiated safety specification. The expansion of this element corresponds to the instantiation of the GSS. An error in this expansion could easily lead to an erroneous proof because the instantiated safety specification is incorrect.

Firstly, the topology translation is diversified (here using a common source) by developing a pair of translators. Here again the expansion is diversified by using two different expanders, in particular to protect the instantiation of the GSS. The two LLL models are as usual checked for equivalence. Finally one of the models is analyzed to prove that the instantiated safety specification holds on the specific design.

The S3 solution has been architectured and developed as a coherent verification solution enabling its use as a class-T2 verification tool in a EN-50128 process for the safety verification of SSIL4 systems. This workflow aims at automating the verification process and eliminating as much as possible the repetitive, time-consuming, expansive, and error-prone human verification activities usually devoted to this task.

Specific S3 Workflows for Interlocking Systems¶

When applied to the alternative IXL development processes described in section Interlocking Development Workflows, the S3 workflows remain fundamentally the same. The design translator is replaced by a second, diversified code translator that can be from another coding language (e.g. the third alternative generating the two implementations in two different languages), or for the same language with diversified sources (e.g. the third alternative generating the two implementations in the same languages), or from a common source but with diversified translators (e.g. the second alternative).

Depending on the coding and design languages, the S3 run to prove the absence of undefined behaviors may be needed or not, on the instantiated design and/or on the vital code.

In some situations, when the safety specification can be connected to both the code and design models, it can make more sense to create combined translators for the code and the specific station topology, yielding simpler version of the workflow mutualizing the two equivalence checks, as shown in the following figure.

Combined Solution Synoptic for Interlocking Systems

Here again, the S3 formal safety verification solution for IXL systems is not to be seen as an off-the-shelf integrated tool, but rather as a collection of generic tools together with protection methodologies enabling Systerel to build custom and efficient solutions targeted at specific missions and IXL systems development processes.

For commercial information and contact see the S3 product page.

Footnotes¶

1: for railway specific terms, see the Interlocking on Wikipedia.
2: The proof of the safety of an RBI is also possible under strict timing hypotheses using approximate modelings.
3: Other processes exist, like complete manual coding, or data-driven systems (e.g. SSI systems), but this section does not address these systems.
4: This instantiation can also be, at least partly, a manual process.
5: Using S3, and bounding the track layout “size”, such a proof is theoretically possible, but it would probably be terribly difficult to achieve.
6: Which may be different from the state seen by the system because of communication latencies and/or sensor failures.
7: Other methods include obtaining this information from a CBTC, ERTMS, or RBC ZC, which are aware of the trains positions, speeds, and braking capacities.