Railway Interlocking Feedback - Revision history

imported>Mathieu: date

2008-10-28T12:57:24Z

date

← Older revision		Revision as of 12:57, 28 October 2008
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	A case study has been carried by [[Systerel]] to verify the DIR 41, a specification of an automated		A case study has been carried by [[Systerel]] in 2007 to verify the DIR 41, a specification of an automated
	interlocking system, by means of system modeling with event-B. This paper gives		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.		an overview of the work done and of some of the results.

imported>Mathieu: DIR 41 definition

2008-10-13T14:57:14Z

DIR 41 definition

← Older revision		Revision as of 14:57, 13 October 2008
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	A case study has been carried by [[Systerel]] to verify the specification of an automated		A case study has been carried by [[Systerel]] to verify the DIR 41, a specification of an automated
	interlocking system by means of system modeling with event-B. This paper gives		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.		an overview of the work done and of some of the results.

imported>Mathieu: link

2008-10-13T14:56:10Z

link

← Older revision		Revision as of 14:56, 13 October 2008
Line 1:		Line 1:
	{{TOCright}}		{{TOCright}}
	A case study has been carried to verify the specification of an automated		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		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.		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		This study was supported by the [http://www.ratp.fr RATP] (French organization in charge of Paris
	transportation).		transportation).

Line 81:		Line 81:
	It is of interest to note that at the end of the study, the results were		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		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		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		scenario they are used to, which come from several decades of field
	feedbacks. Those ''magical scenario'' nonetheless were pertinents.		feedbacks. Those ''magical scenario'' nonetheless were pertinents.
Line 128:		Line 129:
	=== DIR 41 Analysis ===		=== DIR 41 Analysis ===
	Some essential concepts for the railway domain were refined during the study.		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		For example the ''safety statement'' was refined to a ''safety preservation''
			one: the interlocking system actions should not decrease the
	current safety level.		current safety level.

imported>Mathieu: Initial revision : import from abz2008 short paper

2008-10-13T11:49:53Z

Initial revision : import from abz2008 short paper

New page

{{TOCright}}
A case study has been carried 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:
# Writing an autonomous requirements specification approved by the domain experts,
# Designing a refinement plan,
# 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.

<center>
{{SimpleHeader}}
|+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
|}
</center>

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.