imported>Mathieu |
imported>WikiSysop |
| Line 1: |
Line 1: |
| − | {{TOCright}}
| + | #REDIRECT [[Structured Types]] |
| − | 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
| |
| − | an overview of the work done and of some of the results.
| |
| − | | |
| − | This study was supported by the [http://www.ratp.fr 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.
| |
