Railway Interlocking Feedback

A case study has been carried by Systerel to verify the specification of an automated interlocking system by means of system modeling with event-B. This paper gives an overview of the work done and of some of the results.

This study was supported by the RATP (French organization in charge of Paris transportation).

Context and Goals

Some RATP units are responsible for evolution and maintenance of an automated interlocking specification document.

In order to improve their paper and pencil process, RATP asked Systerel if Event-B could be useful to them. An eight month study was launched whose main goal was to help RATP improving their confidence in their interlocking specification, by applying an Event-B approach on rewriting their requirement document.

Description of Work

The main difficulty that arose at the very beginning of the study was to answer the initial question: what does a "working interlocking system" mean?

In an attempt to both answer this question and stay within the expectations of the railway's people, we chose to allocate a great chunk of time to the elaboration of our own requirements specification, by rewriting the RATP specification with the organization and the wording of our choice. This task was carried before doing any modeling work and was aimed at introducing safety principles and safety concepts step by step.

The obtained requirement specification was to be approved by the domain experts and to serve as a reference for the modeling task.

Our modeling process was thus broken down as follow:

1. Writing an autonomous requirements specification approved by the domain experts,
2. Designing a refinement plan,
3. Modeling the system and proving it correct.

The whole process was highly iterative. Indeed, it often appears while modeling that some concepts still need refinements or adjustments which in turn lead to a rework of the refinement plan or the model.

Structure of the B model.

Collision avoidance (2 levels)

Environment structures (5 levels)

Control principles (4 levels)

Instantiation (4 levels) signal switch command transit locking opposing locking

The achieved model, which overall structure is shown in table here before, contains fifteen levels of refinement.

Results

The study led to several interesting results either by giving some clues about a better way for building an event-B model for a real world system, or about the quality of the automated interlocking specification, object of this study.

Organization

Our first intention was to teach some basics of event-B to the domain experts in order to allow them to at least follow, and at best approve, the modeling steps. It proves as a bit utopian. It would certainly have needed a lot more of teaching effort to be efficient.

It is of interest to note that at the end of the study, the results were perceived by the domain experts as magical ones: the failure scenarios exhibited seem to come from nowhere (in fact, proof obligations of the B model that couldn't be discharged), in contrast to the scenario they are used to, which come from several decades of field feedbacks. Those magical scenario nonetheless were pertinents.

Modeling Process

The modeling process we have planned had some place for improvements (some of which were applied during the study). They are summed up hereafter:

Process for Industrial Strength Models

There is a need for a more robust modeling process, perhaps somewhat similar to those being used at the software level. An industrial modeling process probably needs the following phases:

• Requirements specification,
• Validation tests definition,
• Refinement planning,
• Modeling and proving,
• Validating.

The requirements specification rewriting phase done at the beginning of the study involved a lot of refactoring and lead to a final document that was too far from the domain experts expectations to be fully approved. Animation looks like a must have to ease model validation by domain experts.

It is also worth to note that seeking for a posteriori justification, as was done in this study, is very difficult. Indeed, the system was obviously not designed to be proved. In fact, it appears to us that most of existing industrial systems were not designed with validation in mind.

Modeling Techniques

Our model didn't explicitly take into account degraded cases for the system. It proved to be a bad design choice and it was a burden for the proof of the model, as event guards become more and more complex throughout the refinement levels. As a consequence, it appears that models need to be totally closed, and thus should not only take into account the controller and its environment, but also degraded cases.

Models also appears to contribute to at least two goals:

• prove properties over the system modelled,
• help the conceptualization (as an intellectual tool for reasoning)

As a conclusion, we can also say that refinement appears more and more as an essential concept for successful modeling.

DIR 41 Analysis

Some essential concepts for the railway domain were refined during the study. For example the safety statement was refined to a safety preservation one: the interlocking system actions should not decrease the current safety level.

And probably the most prominent result is that four potential safety flaws were exhibited (with an expected low probability of occurrence), which are now being tackled by the RATP teams. It also revealed the existence of several implicit hypotheses on the environment behaviour or on the design of the railway network.

Conclusion

Modeling a system with event B proved to be very interesting for pointing out potential safety flaws and for proving global safety.

This way of modeling allows a B expert with little knowledge in an industrial domain to quickly grasp the domain core concepts. It is still very difficult to involve the domain experts in the whole process and we have high expectations that model animation would improve this.