The radio-controlled railroad crossing was the reference case study of the SoftSpez project funded by the DFG. It was inspired by a new mechanism to control railroad crossings on medium speed routes, i.e., routes with a maximum speed of 160 km/h, proposed by the German rail-way organization. Compared to the original specification, there are some simplifications that reduce the case study's scope and remove some complexities; most importantly, we focus on a single crossing with a single track only. The case study shows how systematic tool-supported modeling increases the comprehensibility and therefore the adequacy of the models as well as the analysis results.

The S# version of the case study can be found here.

The radio-controlled railroad crossing replaces many of the sensors and signals traditionally placed alongside the train tracks by radio communication and software computations with the hope of making the system more robust and scalable. The train control software knows about the locations of the crossings that lie ahead and secures them just in time via wireless communication. Among other problems, the system takes lost communication messages and malfunctions of the crossing into account, causing the train to initiate an emergency stop right before reaching the crossing if it cannot be certain that the barriers are in fact closed. Consequently, safety-critical functionality moves from hardware components to software-based control systems that are specifically designed to avoid potential collisions, i.e., situations in which a train passes an unsecured crossing.

The figure above shows a train approaching a crossing. The danger spot represents a position where the train is considered to reach the crossing, that is, the train may only pass the danger spot if the crossing is secured. When the train reaches the close position, it sends a message to the crossing requesting it to initiate its closing procedure. This procedure takes some time, i.e., the crossing does not immediately enter a secured state as it must first activate its traffic lights before the barriers are allowed to begin closing, which takes some time. Once the barriers are closed, the crossing is secured and the train is allowed to pass. During the time the barriers are closing, the train continues to approach the crossing.

When the train reaches the query position, the control software queries the crossing's state. Usually, the crossing responds with a message indicating that it is secured and that the train can safely pass. If, however, the train does not receive the message before it reaches the stop position, it initiates an emergency stop. There might have been a malfunction that prevented the barriers from closing or the train's closing message was lost, so the train cannot reasonably be allowed to pass the crossing. On the other hand, it is possible that only the crossing's message was lost and the barriers are in fact closed. In that case, the emergency stop is unnecessary, but from the train's point of view, there is no way to tell these situations apart. Consequently, the train must always stop whenever it does not receive a message from the crossing in time, regardless of the potential causes.

The close, query, and stop positions are computed dynamically by the train control software in such a way that there is enough time for the crossing to secure itself before the train passes the danger spot, or in case of any problems, the train is able to stop before reaching the danger spot. In order to compute the close, query, and stop positions, an odometer continuously measures the train's current speed v and position p. Additionally, the train has access to the relevant parameters of all railroad crossings, including the locations of their danger spots dp and the time t they need to secure themselves. All of the calculations take a safety margin m into account in order to compensate for small discrepancies in p and v due to inaccurate measurements by the odometer. The stop position is constantly updated such that the train is always able to fully stop before dp, that is, stop := dp - m - v^2/(2a) where a is the train's maximum declaration. The query position depends on the stop position: The time it takes the train to travel the distance between both positions must be greater than the time it takes to query the crossing's state, so query := stop - 2cv where c is the maximum expected communication delay. Similarly, the close position depends on the query position, as the train must allow the crossing to secure itself before it queries the crossing's state: close := query - v(t + c).

There is a sensor behind the crossing that signals the crossing to open once the approaching train has passed by. The sensor and the crossing are connected by wire. Usually, the barriers remain closed until the approaching train passes the sensor. There is an exception, however: If the train takes too long to reach the crossing, the barriers open regardless of the train's position. This seemingly counterproductive behavior is justified by the observation that the longer the barriers are closed, the more likely it is that some drivers ignore them, i.e., drive around them and pass the secured crossing. Due to this human factor, it is preferable to open the barriers after a certain period of time rather than increasing the likelihood of this uncontrollable situation.

We consider the seven faults depicted in the above figure: The odometer might report incorrect position or speed values (position and speed, respectively). The train's brakes might malfunction, preventing the train from stopping (brakes). The sensor checking whether the barriers are closed might incorrectly report that non-closed barriers are closed or vice versa (report state) or the barrier motor might get stuck, preventing the barriers from opening or closing (move). Lastly, the sensor that causes the crossing to be opened again might incorrectly report that the train has passed (detection) or communication messages transmitted via radio might get lost (message).

Collision avoidance is the system's primary safety goal, i.e., the system is designed to avoid the hazard of a train passing an unsecured crossing. A hazard concerning the erratic human behavior mentioned above occurs if the barriers remain closed for longer than absolutely necessary. These two hazards are antagonistic, as the former can be avoided by never opening the barriers while the latter is made impossible by never closing them. Therefore, a tradeoff must be found that balances both hazards. In the remainder, we restrict the discussion to the first hazard, that is, the hazard of collisions. To do that, we focus on the behaviors of the train and crossing controllers as well as the messages passed between them over radio, ignoring details such as traffic lights or the technical protocol used by the communication channel.

In contrast to the other case studies, the radio-controlled railroad crossing has two physically separate controllers that have to be modeled separately and combined together via a communication channel. Other than that, however, no special modeling language support is required, so the challenge primarily lies in the systematic creation of a comprehensible model such that the hazard can be analyzed in an adequate way.