Early Detection of Design Flaws in Transportation System Specification Process

From Evidence on Formal Methods Uses and Impact on Industry
Jump to: navigation, search
Success Story
Domain Transportation
Keywords Event-B, railway system, specification, safety case, CBTC
Source SYSTEREL

Main -> DEPLOY Success Stories -> Transport-3

Short Description

Puzzle-s.png

The development of highly constrained systems requires advanced studies and rigorous approaches, in order to produce high-quality systems. Event-B [1], as a formal method for system-level analysis, provides a mathematical way to understand the considered system and mitigate hazards, by modeling it and proving the associated safety requirements.

SYSTEREL, a SME specialized in safety-critical embedded systems, worked in 2010 on a large system, and more precisely a Zone Controller (ZC) sub-system of a Communications-based train control(CBTC) system, for a new actor of the railway industry, using this method. The safe behavior of a CBTC system regarding particular aspects, such as train tracking or collision avoidance, is defined by a set of required safety properties. The modeling/proving activities performed after having clearly defined these safety properties, allowed to safely design and interface the ZC sub-system.

Related FAQ

of Interest to Project and QA Managers

  • QI-PQAM-2 How is the productivity of the various stages of the system development cycle affected when formal engineering methods are used ?
  • ExFac-HM-1 What is the position of standards regarding formal methods in my Industry segment? (e.g. are they enforcing, highly recommending, etc.)

of Interest to Engineers and Analysts

  • TOOL-EA-2 Are tools functionality automating all tedious tasks?

Benefits

  • Formal validation of system models according to safety properties, in interaction with the system design and specification in natural language.
  • Design flaw detection at system specification level (including faulty scenario expression, missing hypotheses...).
  • System design is guided by the Event-B method so that its architecture is better defined and concerns get better isolated.

Limitations

  • Previous safety properties analysis must be exhaustive (i.e. modeling and proving do not allow to find missing safety properties).
  • At the current time, some further consolidation of the existing tools is required to ease these tasks.
  • The modeler could feel isolated when trying to make some important decisions about modeling, as there is currently a lack of expertise and know-how in industrial size applications of the method.
  • Difficulties to convince the decision makers to adopt the Event-B method, and to share the model and the obtained results with domain experts without mathematical knowledge.

Elaboration

This task was uncommon and innovative in many respects:

  • In France, the opportunity to entirely develop such a system is rare! Historical actors of the railway industry commonly carefully monitor the evolution of their existing CBTC systems to mitigate risks and preserve the safety demonstrations.
  • In the railway domain, the benefits of the B method are generally acknowledged for correct-by-construction software development. However, the Event-B method, whose purpose is to model full systems, is not currently well known. The system specification, expressed in natural language, is usually validated using dedicated safety studies or tests. Although the activities of modeling and proving with Event-B, which formalize the safety properties and the essential elements of the studied sub-system, does not replace for example a FMEA analysis, it demonstrates that the safety properties hold under some well-defined hypotheses.
  • The experience in complex transportation systems has shown that the commonly-used process often reveals its permeability to design flaws, detected lately at further levels of development, or several years after the starting date. The chosen approach was a pioneer approach, where Event-B was used during the specification phase. Thus, it allowed an early detection of such issues.
  • The modeling and proving activities had a direct interaction with the system design and lead to several evolutions or corrections.
Context of the Formal Verification Work

The main arguments of this study and lessons learned are detailed here:

  • To ease the proofs of safety properties, the models were defined as abstractions which conformed to the system. In these abstractions, only the necessary modeling elements requested to prove the safety properties were represented. This abstraction was mandatory to ensure the provability of models for such big systems.
  • The other side of the coin is that such an abstraction requires confidence in the model representativity (does my model fit the reality?). Hence, beside the main modeling/proving activities, the models were rendered using a 3D animation (AnimB plug-in for the Rodin platform).
  • It was important to perfectly well understand and respect the principles of the Event-B method, in particular to avoid dead-end proofs. As a consequence, the modeling choices were permanently reconsidered and reviewed during the project lifecycle. On the contrary, it could not be concluded, when facing a difficulty, that the method or the tool has to adapt to these previous choices.
  • The work of modeling and understanding the proofs lead to a better understanding of the system. It eased the definition of clear concepts and the separation of the system into modules with a better separation of concerns, so that the obtained architecture is clearer than the one obtained without modeling. It comes from the fact that proofs must remain simple and clear, which forces the modeler to keep his models the simplest and the clearest. Moreover, some assumptions derived from the modeling directly impacted the design. For example, the need to permanently track trains on the discretized railway (using envelopes).
  • The Event-B modeling can be considered as a R&D task. It was a real challenge to manage such activity in an industrial context, as the Event-B modelers do not know accurately in advance how much time they will need and what will precisely be the output of their modeling and proving activities.

Related Work

N/A

Specific DEPLOY Contributions

  • Use of the DEPLOY-supported Open-Source RODIN platform as a tool to model and prove using Event-B Rodin-s.png
  • Feedbacks to enhance the performance of the Rodin platform,

which have been captured and which influenced the 2.x releases of the platform.

Further work

The work presented here can be considered as state-of-the-art. It has consolidated the expertise of SYSTEREL in applying the Event-B method during system specification of industrial size projects. This knowledge will be an advantage for further applications.

References

  1. Jean-Raymond Abrial, Modeling in Event-B: System and Software Engineering, Cambridge University Press, 2010.
Personal tools
Namespaces
Variants
Actions
Navigation
Toolbox