[Sujet Thèse 2020] Validation de spécifications Event-B: prise en compte du raffinement

Contexte scientifique

Le caractère multifacette et la complexité des systèmes développés augmente. La notion de développement avec utilisation de méthodes formelles et de modèles abstraits est importante. La validation des modèles formels devient une question cruciale tant pour la correction du logiciel final que pour son développement. La dernière décennie a vue des avancées importantes dans le domaine de méthodes formelles dites {model-based par la mise à disposition d’outils utilisables pour assister le développeur sur trois plans en parallèle :

  • la vérification des modèles formels [1],
  •  la validation des modèles formels [7, 4, 5, 3],
  • l’expression des liens entre l’expression des besoins et le modèle formel [2, 6].

Avec ces trois types d’outils, il est possible de mettre en place une
procédure de validation d’un modèle formel particulier. Néanmoins, il manque aujourd’hui la prise en compte de la dynamique du développement de la spécification, c’est-à-dire de l’évolution du modèle lors de son raffinement.

Le raffinement formel, tel que défini en B ou B-événementiel par exemple, permet de vérifier la spécification à chaque étape de son développement. Il est ainsi possible d’assurer que le travail avance vers une solution sûre en prouvant les relations entre les états successif du modèle. L’ambition de ce travail est d’offrir une telle assurance quant à la  validité des modèles successifs. Le principe de base est d’identifier une forme  d’incrément de couverture des besoins, grâce notamment à la gestion des liens entre besoins et éléments du modèle formel, et de valider par rapport à cet incrément. Ainsi, la procédure générale de validation serait liée au raffinement du modèle.

Sujet de thèse

Le sujet proposé s’inscrit dans la continuité directe des travaux cités ci-dessus. Les questions auxquelles la thèse devra plus
particulièrement contribuer à répondre sont les suivantes:

  •  Comment associer le raffinement formel à l’extension de la couverture des besoins? En particulier, comment représenter cette relation avec la notion des liens étudiés par I. Sayar?
  • Comment associer les incréments de couverture aux actions de validation, notamment la définition de scénario d’exécution du modèle?
  • Quelles conditions et propriétés doivent respecter les incréments de couverture pour assurer que la validation de la spécification finale soit l’accumulation des validations de chaque raffinement?

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 B-événementiel. 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éroulera dans l’équipe MOSEL-VERIDIS, département “Méthodes Formelles” du LORIA.

Encadrement

Le travail sera encadré pas J. Souquières, professeur, et J.-P. Jacquot, maître de Conférences.

Références

[1]  Jean-Raymond Abrial. Modeling in Event-B : System and Software Engineering. Cam- bridge University Press, 2010.

[2]  Fahad R. Golra, Fabien Dagnat, Jeanine Souquières, Imen Sayar, and Sylvain Guerin. Bridging the Gap between Informal Requirements and Formal Specifications Using Model Federation. In SEFM 2018 International Conference on Software Engineering and Formal Methods, Toulouse, France, pages 44–69, 2018.

[3]  Jean-Pierre Jacquot and Atif Mashkoor. The Role of Validation in Refinement-Based Formal Software Development. In Atif Mashkoor, Qing Wang, and Bernhard Thalheim, editors, Models : Concepts, Theory, Logic, Reasoning and Semantics – Essays Dedicated to Klaus-Dieter Schewe on the Occasion of his 60th Birthday, pages 202–219, 2018.

[4]  Atif Mashkoor, Faqing Yang, and Jean-Pierre Jacquot. Refinement-based Validation of Event-B Specifications. Software and Systems Modeling, 16(3) :789–808, 2017.

[5]  Imen Sayar and Jeanine Souquières. La validation dans les premières étapes du processus de dévelopement. Revue ISI-DAT, numéro spécial ”Décisions, argumentation et tracabilité dans l’Ingénierie des Systèmes d’Information”, 22(4) :11–41, 2017.

[6]  Imen Sayar and Jeanine Souquières. Bridging the Gap Between Requirements Document and Formal Specifications using Development Patterns. In IEEE 27th International Re- quirements Engineering Conference Workshops (REW), pages 116–122, 2019.

[7]  Faqing Yang, Jean-Pierre Jacquot, and Jeanine Souquières. Proving the Fidelity of Simu- lations of Event-B Models. In 15th International IEEE Symposium on High-Assurance Systems Engineering, Miami Beach, FL, USA, January 9-11, pages 89–96, 2014.

Aucune offre n'est disponible pour l'instant.

Logo d'Inria