[PHD 2019] Relation between Validation and Refinement in Event-B

Advisors : Jeanine Souquières and Jean-Pierre Jacquot 

LORIA –  http://dedale.loria.fr 

Scientific Context and State of the Art.

Programs in either purely software systems or in cyber-physical systems are more and more required 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 modelled and their properties can be assessed. We can then ensure that safety invariants are maintained while the systems are running.

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 [10, 11, 12] 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 observation levels to guide the refinement, [4, 6]. 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 [3, 8, 9].   

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 mentioned 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 requirements 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. Former work, [2] and [5] for instance, has shown the pertinence of refinement-base methods, as well as their current short-comings.

References

[1] J. R. Abrial.  Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.

[2] F. Boniol and V. Wiels.  Landing Gear System case Study, ABZ Case Study, Berlin, Communications in Computer and Information Science, Springer, vol. 433, p. 1-18, 2014.

[3] F. R. Golra, F. Dagnat, J. Souquières, I. Sayar and S. Guérin. Bridging the gap between informal requirements and formal specifications using model federation. Vol. 10886 of LNCS. SEFM 2018 International conference on Software Engineering and Formal Methods, June 2018, Toulouse, Fr.

[4] A. Mashkoor. Ingénierie Formelle de Domaines : Des Spécifications à la validation. PhD thesis, Université de Nancy 2, 2011.

[5] A. Mashkoor. The Hemodialysis Machine Case Study. In Actes ABZ, p. 329-343, Linz, Austria, 2015.

[6] A. Mashkoor, F. Yang, J.-P. Jacquot. Refinement-based Validation of Event-B Specifications Software and Systems Modeling, Springer Verlag, 2016, pp.33.

[7] A. Mashkoor, J.-P. Jacquot. Validation of Formal Specifications through Transformation and Animation Requirements Engineering, Springer Verlag, 2017, 22(4), pp.433-451.

[8] I. Sayar et J. Souquières. La validation dans les premières étapes du processus de développement. Numéro spécial « Décisions, argumentation et traçabilité dans l’Ingénierie des Systèmes d’Information ».  Revue ISI-DAT, volume 22, pp. 11-41 – n° 4/2017.

[9] I. Sayar. Articulation entre activités formelles et activités semi-formelles dans développement de logiciels. PhD thesis, Université de Lorraine, mars 2019.

[10] F. Yang, J.-P. Jacquot, and J. Souquières. The Case for Using Simulation to Validate Event-B Specifications. In Pornsiri Muenchaisri Karl Leung, editor, APSEC2012 – The 19th Asia-Pacif Software Engineering Conference, Hongkong, Chine, 2012.

[11] F. Yang, J.-P. Jacquot, and J. Souquières. Proving the Fidelity of Simulations of Event-B Models. The 15th IEEE International Symposium on High Assurance Systems Engineering (HASE), Jan 2014, Miami, United States.

[12] F. Yang. A simulation environment for the validation of Event-B specifications. PhD thesis, Université de Lorraine, 2013.

Logo du CNRS

Logo d'Inria

Logo Université de Lorraine