1 Introduction
1.1 ETCS levels 1–3
1.2 Hybrid level 3
1.3 Virtual block function for HL3
2 Formal language and tools used
Symbol | Math | Meaning |
---|---|---|
! | \(\forall \) | Universal quantification |
# | \(\exists \) | Existential quantification |
& | \(\wedge \) | Conjunction |
or | \(\vee \) | Disjunction |
=>
| \(\Rightarrow \) | Implication |
= | \(=\) | Equal |
/ = | \(\ne \) | Not equal |
: | \(\in \) | Set membership |
/ : | \(\notin \) | Not in set |
\({\texttt {<:}}\) | \(\subseteq \) | Subset |
{} | \(\emptyset \) | Empty set |
{x|P} | \(\{x\mid P\}\) | Set defined by predicate P |
\(\backslash {/}\) | \(\cup \) | Set union |
\({/}\backslash \) | \(\cap \) | Set intersection |
\(\setminus \) | \(\setminus \) | Set difference |
UNION | \(\bigcup \) | Quantified union |
\({\texttt {|->}}\) | \(\mapsto \) | Pair constructor |
dom(r) | Domain of a function or relation r | |
ran(r) | Range of a function or relation r | |
f(x) | Application of a function f to x | |
size(s) | Length of a sequence | |
INTEGER | \({\mathbb {Z}}\) | Set of mathematical integers |
NATURAL | \({\mathbb {N}}\) | Set of natural numbers (\(\ge 0\)) |
POW(S) | \({\mathbb {P}}(S)\) | All subsets of S |
\({\texttt {<->}}\) | \(\leftrightarrow \) | Relation |
- ->
| \(\rightarrow \) | Total function |
\({\texttt {+->}}\) | Partial function | |
seq(S) | Set of sequences over S | |
iseq(S) | Set of injective sequences over S (i.e., no repetitions) |
2.1 Some background about B
- new base sets.
- constants along with axioms (aka PROPERTIES) which describe the types and allowed values for the constants.
- variables along with invariants which describe the type and allowed values for the variables.
- operations which can change the values of the variables of the machine. Operations can take parameters and may have guards, i.e., predicates which state when they are enabled and can be executed. In the context of systems modelling operations are typically called events.
TRAIN
and REPORTED
_TRAIN
_INTEGRITY
. The first one is called a deferred set: its members are left open and can be specified at a later point in time. The second one is fixed and called an enumerated set: all its members are provided. The machine has no constants but two variables along with invariants. The variable registered
is a subset of TRAIN
and the variable status is a total function from the registered trains to their integrity status. The operation register
_train
adds a new train to registered
and sets its status to no
_integrity
_information
. The operation is enabled when there exists a train tr
which is not yet registered. The body of the operation is executed atomically, resulting in a final state where both registered
and status
are updated and the invariant holds.
3 Core concepts of HL3
- free: the VSS is guaranteed to be free;
- occupied: the VSS is occupied by a communicating train and nothing else;
- unknown: the VSS is not occupied by a communicating train, but may be occupied by other non-communicating trains or obstacles;
- ambiguous: : the VSS is occupied by a communicating train, and may also be occupied by other non-communicating trains or obstacles.
# | Condition | Priority over | Section ref. |
---|---|---|---|
#9A | (TTD is free) | 3.1.1.5 | |
#9B | (integer train has reported to have left the VSS) | #10 | 4.5.1.7 |
AND (the shadow train timer A of the TDD was not expired at the moment of | |||
the time stamp in the position report) |
4 Requirements and modelling strategy
- The Thales RBC core was to be used as is, without modifications for HL3. (Thales owns a product line for the RBC software to configure the generic software to the project specific requirements).
- The interlocking was used as is, without modifications for HL3.3
- The VBF had to be developed from scratch as an add-on for the RBC, which was to mimic an interlocking and transmit the signal aspects for the virtual signals to the RBC. The VBF contains a VSS state machine, with four possible states (free, occupied, unknown and ambiguous) for each VSS, exactly as required by the HL3 specification.
X
can be found in the folder of the same name X
, while the contents of a package X
.Y
can be found in the folder Y
within the folder X
.main
directory:
test
/environment
:
test
/environment
, such as test
/environment
/ENIF
for the on-site field tests:
- a very simple topology,
- the topology from the HL3 specification (HL3),
- the actual topology to be used for the on-site field tests (ENIF).
- as the name of B operations. For example, the transition 9A from ambiguous to free is modelled by the B operation
VSS
_Ambiguous
_Free
_9A
. - some higher-level operations, which collect updates to the various VSS, return the track name and transition number (such as 9A) as return result, which can be inspected in the ProB animation interface.
- label pragmas that precede predicates. This is useful for requirements identifiers or links to sections in the requirements document. The syntax of this kind of pragma is:$$\begin{aligned} {\texttt {/*@label ``LABEL'' */}} ~{ Predicate}. \end{aligned}$$
- description pragmas that follow predicates and identifiers. This is useful for longer justifications or explanations. Such a pragma looks like the following:$$\begin{aligned} { Formula}~ {\texttt {/*@desc ``DESC'' */}}. \end{aligned}$$
5 Model details
5.1 Basic datatypes
next
_vss
constant is a partial function which links VSS to their successor VSS. The direction of the track is thus constant for any given execution run.5 However, the direction of the track can be toggled after executing a scenario, since the conversion of the XML data is parameterised. Below we show how the next
_vss
constant is derived in another B machine. Observe that we allow the IF-THEN-ELSE to be applied to expressions and use an external B function (see Section 6.3 in [17]) to read in the track data from an XML file.
5.1.1 Train status
TRAIN
_INTEGRITY
_MAPPING
. However, the HL3 specification only distinguishes between three values, which are represented by the enumerated set REPORTED
_TRAIN
_INTEGRITY
. The surjective function TRAIN
_INTEGRITY
_MAPPING
defines the respective mapping bridging the gap between these two specification documents. Note, that this is not the only possible mapping as an infrastructure manager could require to map TRAIN
_INTEGRITY
_CONFIRMED
_BY
_DRIVER
to no
_integrity
_information
to exclude human failure.INTERNAL
_TRAIN
_INTEGRITY
in our model.6 The conditions of the state machine in the HL3 specification are referring to this integrity state. Yet, an unambiguous mapping from the reported train integrity to the internal train integrity is missing in Sect. 3.5. Thus, we were forced to find a sensible interpretation; we defined the following two conditions as triggers for the transition from “integer” to “non-integer”:- “train reports ‘lost integrity’ ”
- “PTD [Positive Train Detection] with no integrity information is received outside of the integrity waiting period”
train
_reportedTrainIntegrity
is not a total function with the registered trains as its domain. As a consequence, we had to make a further decision by treating a train as non
_integer
before the VBF receives the first position report (interpretation to the safe side). We always tried to avoid partial functions as it would mostly introduce handling of special cases. Moreover, the description in the HL3 specification is imprecise regarding when to start the first “wait integrity timer”: “A ‘wait integrity timer’ runs continuously for every train [...]” [1, Section 3.4.1.3.1]. We decided to start the timer with first train position reported but not with the registration.5.1.2 Train location
train
_location
as a total function from registered trains to sets of VSS is very convenient. Alternatively, we could have used a relation from trains to VSS, but we generally preferred functions over relations. One exception is the next
_vss
constant binary relation between VSS, which is frequently inverted in our model and can be obtained using B’s relational inverse operator: next
_vss
\(\sim \).7 The order of the VSS associated to a train is not incorporated into the train
_location
definition, as this information is already contained in the next
_vss
constant relation. The condition that a train location must not have any gaps (which is not explicitly mentioned in the HL3 specification) can also easily be expressed with the aid of next
_vss
as follows:
loc
corresponding to a set of VSSs, there must exist an ordering of the VSSs (i.e., an element of iseq(loc)
) such that these are chained together by the next relation (i.e., next
_vss
). Remember that Table 1 contains a brief explanation of the B operators used in this article.- Minor: “As long as the TTD where the max safe front end is reported is free, the train location is not extended onto the VSS which are part of this free TTD” [1, Section 3.3.2.1.2]. This is imprecise as the condition should be: only if the max safe front is reported to be on the next free TTD but not the estimated front of the train.
- Fundamental: “[...] the train location is derived from the estimated front end [...] of the last position report [...] as well as from TTD information [...].” Is the train location only updated/changed by processing train position reports (in this case the TTD information will of course be considered)? Or does a single TTD change event without a train position report also update the train location? We had tried both alternatives and in the end we decided to use a train position report as the only trigger to update the train location (as used by the first demonstrator in December 2017). The other alternative would have forced us to adapt several transitions in order to be able to replay all scenarios of the HL3 specification (version 1A). Note, that the authors of the HL3 specification then decided on the other alternative in version 1B which was released in April 2018. As it was a fundamental change, it resulted in a lot of inconsistencies between the state machine and the scenarios which were not solved until version 1C (also thanks to our comments). But in the end, we think the authors’ decision was the right one.
5.2 State machine transitions and priorities
Guard9A
which captures the conditions under which transition 9A is applicable.VSS
_Statemachine
_Step
) which includes VSS
_StateMachine
and which encodes the priorities using a nested IF-THEN-ELSE statement using the guard definitions.VSS
_Statemachine
_Run
) which includes VSS
_Statemachine
_Step
and executes all update steps until completion using a WHILE loop.2A
has priority over 3
, as requested by [1]. A return variable out
stores the exact VSS transition taken for debugging and analysis. Here we show part of the corresponding operation:
VSSUpdateStep
.8 Again, the output changes
is for debugging with ProB, to be able to see the VSSs that have changed their status and which HL3 transition was applied to perform the change.
5.3 Modelling of time
currentTime
. The progress of time is modelled by calling an operation UpdateCurrentTime
which obtains the new time as an input and also updates the set of expired and running timers. It is the only way time can be modified in our model. During actual execution of our B model, the surrounding Java program was responsible for regularly calling the UpdateCurrentTime operation with the current system time in milliseconds as parameter.6 Validation and verification
6.1 Animation of scenarios
The problem with transition #11A is that it contains an additional third condition which is not part of transition #9B: “the reported min-safe-rear-end of this train is within the distance that can be covered at the reported speed within the “shadow train timer A” from the TTD limit”. If this condition is not satisfied, our logical implication (**) stated above will not hold. In the scenario, this violation of the implication would lead to the case that VSS32 would not go to “occupied” but to “ambiguous” while VSS31 would still go to “free”. While “ambiguous” means that there is a shadow train risk, “free” means that there is no shadow train risk and the VSS is released for following trains. We eliminated this inconsistency by adding the third condition of transition #11A to transition #9B because it provides an additional check against shadow trains.If transition #9B is applied to a VSS, then transition #11A should be applied to the next VSS (if we neglect the fact that #9B could also be applied to the next VSS).
6.2 Tooling enhancements
6.2.1 Replaying recorded runs with ProB
6.2.2 HTML export
6.3 Further validation activities
6.3.1 Constraint-based analysis
6.3.2 Model checking
6.4 Visualisation
- We quickly spotted mistakes in the specification and the model.
- We used the visualisation to communicate the model within our team and to the domain experts.
- We were able to replay the scenarios in the HL3 specification and detected inconsistencies between them and the state machine description.