[Thèse 2019] Etude de la validation de spécifications formelles

Directeurs de thèse: Jeanine Souquières et Jean-Pierre Jacquot (http://dedale.loria.fr)

 

Contexte scientifique. La complexité des systèmes développés augmente et l’utilisation de méthodes formelles dans son développement est très importante. La validation des modèles formels devient une question cruciale tant pour la correction du logiciel final que pour son développement.

Le processus de développement à l’aide du raffinement utilisé dans B ou Event-B [1] est comparable à un processus de la cascade : le modèle initial fixe l’invariant que l’implantation doit garantir et chaque raffinement est à nouveau prouvé dans l’invariant abstrait. De telles approches assument trois propriétés: nous avons toutes les exigences pour décrire le modèle initial, le modèle initial est une description formelle adéquate des exigences de sécurité et fonctionnelles et toutes les décisions prises pendant le raffinement peuvent être conservées selon une exigence. En pratique, peu de développements décrivent entièrement de telles propriétés : les exigences évoluent avec le développement, toutes les exigences ne peuvent être exprimées dans le modèle initial, de nombreux raffinements présentent de nouvelles informations dans le modèle.

Pour aborder le problème décrit ci-dessus, les activités de validation et de vérification doivent être associées à chaque étape de raffinement. Parmi les techniques de validation de modèles, leur exécution est plus attrayante, particulièrement dans le cadre de la modélisation à base de modèles Event-B. La plus grande difficulté vient du non-déterminisme de la plupart des modèles raffinés. En fait, il est recommandé de réduire l’abstraction et le non-déterminisme pas-à-pas. Tandis que des outils actuels, tels que ProB utilisable sous Rodin (http://www.event-b.org), peuvent animer des modèles avec un non-déterminisme modéré, ils ne peuvent pas toujours traiter l’ensemble des problèmes soulevés. Des stratégies d’exploration exhaustives tombent rapidement dans l’explosion combinatoire.

Pour de tels modèles abstraits, une approche raisonnable est de valider la partie limitée de l’espace correspond à la partie intéressante du modèle. Nos travaux récents nous conduisent à trois questions relativement à la validation. Le premier concerne les outils qui permettent d’exécuter les modèles abstraits durant le développement. Avec l’outil JeB [10, 11, 12] défini par F. Yang, il est possible d’observer le comportement des modèles. La deuxième question concerne l’introduction progressive des propriétés formelles dans une façon ordonnée. Les niveaux d’observation guident le raffinement [4, 6, 7]. La troisième question concerne l’élicitation et la formalisation des besoins du client. Les études de cas montrent le potentiel des outils tels que ProR utilisable sous Rodin (http://www.event-b.org) pour lier besoins, modèles formels et raffinement [3, 8, 9].

Sujet de thèse. L’objectif est de détecter les erreurs des exigences lors de la construction incrémentale, via les raffinements: il est important de détecter les anomalies dans les modèles et de les corriger. La spécification finale doit être prouvée pour garantir les propriétés critiques. Le travail se déroulera selon plusieurs axes:

  • Définition de la notion de validation. Est-elle comme la vérification? Est-il possible de décrire la relation entre la validation de la spécification finale et la suite des validations de chaque modèle intermédiaire? Est-il possible de valider un raffinement ou bien le produit obtenu?
  • Etude de méthodes de validation dans le processus de développement avec utilisation d’outils existants.
  • Etude de la « monotonicité ».

Ce travail sera illustré par une étude de scénarii, par exemple autour du flocking et de la plateforme Aetournos du LORIA [12], de l’étude de cas du train d’atterrissage proposée à la conférence ABZ’2014 [2] ou l’étude de cas d’une machine d’hémodialyse proposée à la conférence ABZ’2016 [5]. 

Connaissances et compétences requises. Le sujet se situe à la croisée de deux problématiques, la définition d’outils pragmatiques et les méthodes formelles. Pour cela, il convient de maîtriser les concepts mathématiques qui permettent d’utiliser efficacement les langages de spécifications formels tels que B ou Event-B. La connaissance des outils comme Rodin (http://www.event-b.org), l’atelier B ou, plus généralement, les outils d’assistance à la preuve, serait appréciable.

Le travail se déroule dans le département Méthodes Formelles du LORIA.

Références

[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