PhD Thesis Relation between Validation and Refinement in Event-B

Encadrants : Jeanine Souquières, Jean-Pierre Jacquot — équipe DEDALE

En collaboration avec : Dr Atif Mashkoor —  SCCH, Hagenberg, Austria

 Scientific Context and State of the Art

Programs in either purely software systems or in cyber-physical systems are more and more re- quired to be correct. The costs, both in life and economic loss, are no more acceptable. Formal methods are an answer. They provide us with frameworks where the systems can be modeled and their properties can be assessed. We can then ensure that safety invariants are maintained while the systems are runing.

With a broad brush, formal methods can be classified in two categories: those where properties are established through exhaustion of all states (model-checkers) and whose where properties are logically established (provers). Event-B [1] belongs to the later category.

Proving a program amounts to proving that the properties expressed in the specification can be demonstrated from the text of the program. This implies that the specification must be formally expressed. Such a proof is a very hard task as programs are finely detailed models, far away from the abstract invariant properties of the systems. Event-B and its notion of refinement cover both topics. A development in Event-B goes as follows:

  • the specification is formalized as a highly abstract model with states, events, and invariants to express the safety properties; the proof of internal consistency of the model ensures its correctness,
  • the model is then slowly reified, one step at a time called a refinement; internal consistency and consistency with the previous model must be proven,
  • at the end, the last model is a program (or close to) and is guaranteed to maintain the properties of the initial model.

The huge advantage of this approach is that the verification, i.e. the proof of correctness, is broken into many, smaller, easier to discharge proofs. Verification is thus monotonic wrt refinement as the proof of the final model is the result of the proofs of all the preceding refinements. Mature environments, such as Rodin (http://www.event-b.org), address this issue. However, to diffuse into industry, they must also address the issue of validation.

Validation is the operation which assesses that a formal model is a reasonable description of the world, or, in the case of engineering, a reasonable description of the users’ needs. Our recent works tackled three questions connected to validation. The first concerns the tools to execute the abstract models during the development. With JeB [7, 9, 8] created by F. Yang, it is possible to observe the behavior of the models. The second question concerns the progressive introduction of the formal properties in an orderly manner. We introduced ideas such as observation levels to guide the refinement[5, 2]. The last question concerns the elicitation and formalisation of users’ requirements in a framework consistent with Event-B. Case-studies showed the potential of tools such as ProR(http://wiki.event-b.org/index.php/ProR) for linking requirements, formal models, and refinements [6].

PhD Subject and Working Context

The proposed subject is to study the relation between refinement, as defined with Event-B, and validation. The goal is to define the conditions under which validation would be monotonic wrt refinement. Validation of the final model is the result of the validation of each of the refinements.

The work can be considered as an integration of the answers to the three questions we men- tioned above into a consistent framework. Validation scenario, i.e. a test for a specific property, should be the central notion. It should be built around the idea of increment in covered require- ments linked to a strengthening of the model’s invariant. It should also be associated with the test-like elements that can be run with JeB.

An essential element of our research work is the development of case-studies to induce and assess the design of the framework. The connection of SCCH with medical devices providers provides us with a unique opportunity of validating our ideas with real, hard, case-studies [4, 3]. Regular stays in Hagenberg (near Linz) are expected during the PhD.

References

  • [1]  Jean-Raymond Abrial. Modeling in Event-B : System and Software Engineering. Cambridge University Press, 2010.
  • [2]  Jean-Pierre Jacquot. Premières leçons sur la spécification d’un train d’atterrissage en B Événementiel. Technique et Science Informatiques, page 25, 2016.
  • [3]  Atif Mashkoor. Abstract State Machines, Alloy, B, TLA, VDM, and Z : 5th International Conference Proceedings. chapter The Hemodialysis Machine Case Study, pages 329–343. Springer International Publishing, 2016.
  • [4]  Atif Mashkoor, Miklos Biro, Marton Dolgos, and Peter Timar. Refinement-Based Development of Software-Controlled Safety-Critical Active Medical Devices. In Software Quality. Software and Systems Quality in Distributed and Mobile Environments, volume 200 of Lecture Notes in Business Information Processing, pages 120–132. Springer International Publishing, 2015.
  • [5]  Atif Mashkoor and Jean-Pierre Jacquot. Observation-level-driven Formal Modeling. In 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), Daytona Beach, USA, 2015.
  • [6]  Imen Sayar and Jeanine Souquières. La validation dans le processus de développement. ISI-DAT – Numéro spécial Décisions, argumentation et traçabilité dans l’ingénierie des systêmes d’inforamtion, page 30, 2017.
  • [7]  Faqing Yang. A Simulation Framework for the Validation of Event-B Specifications. Thèse, Université de Lorraine, November 2013.
  • [8]  Faqing Yang, Jean-Pierre Jacquot, and Jeanine Souquières. The case for Using Simulation to Validate Event-B Specifications. In Software Engineering Conference (APSEC), 19th Asia-Pacific, volume 1, pages 85–90, 2012.
  • [9]  Faqing Yang, Jean-Pierre Jacquot, and Jeanine Souquières. Proving the Fidelity of Simulations of Event-B Models. In The 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), Miami, USA 2014.

En ce moment

Logo du CNRS
Logo Inria
Logo Université de Lorraine