These Relation entre la validation et le raffinement en B-Événementiel

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

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

Contexte scientifique et état de l’art

Les programmes, tant dans les systèmes purement logiciels que dans les systèmes hybrides, ont de plus en plus l’obligation d’être corrects. Le coût, humain comme économique, des erreurs est devenu inacceptable. Les méthodes formelles sont une réponse. Elles fournissent des environnements dans lesquels les systèmes peuvent être modélisés et leurs propriétés peuvent être évaluées. Nous pouvons alors garantir la sécurité tout au long de l’exécution du système.

Grossièrement, les méthodes formelles peuvent être classées en deux grands catégories : celles qui vérifient les propriétés par une exploration exhaustive des états du système (avec des model- checkers) et celles qu  établissent lespropriétés par des preuves (avec des provers). B-Événementiel [1] fait partie de la seconde classe.

La preuve d’un programme revient à établir que les propriétés exprimées dans la spécification peuvent être démontrées à partir du texte du programme. Premièrement, ceci implique que la spécification doit être exprimée formellement. Deuxièmement, une telle preuve est notoirement difficile du fait que les programmes sont des modèles extrèmement détaillés, très éloignés des propriétés invariantes abstraites du système. B-Événementiel et la notion de raffinement répondent aux deux problèmes. Un développement avec B-Événementiel se déroule de la façon suivante :

  • –  la spécification est modélisée sous la forme d’un modèle abstrait comportant des états, des événements et des invariants pour exprimer les propriétés de sécurité ; la preuve de cohérence interne du modèle établit sa correction,
  • –  le modèles est ensuite réifié lentement, une étape à la fois, appelée un raffinement; la cohérence interne et les relations avec le modèle précédent doivent être prouvées,
  • –  à la fin, le dernier modèle est un programme (ou très proche d’un programme) qui garantit les propriétés  exprimées dans le modèle initial.

Le grand avantage de cette approche est que la vérification, c’est-à-dire la preuve de la correction, est divisée en de nombreuses preuves, plus courtes et plus faciles à établir. Nous avons ainsi la monotonicité de la vérification par rapport au raffinement, puisque la preuve du modèle final est le résultat des preuves de tous les raffinements précédents. Des ateliers comme Rodin (http: //www.event-b.org) offrent le support nécessaire sur ce point. Néanmoins, pour qu’ils diffusent dans l’industrie, ces ateliers doivent aussi offrir un support pour la validation.

Le validation assure qu’un modèle formel est une description adéquate d’un phénomène naturel, en sciences, ou des besoins des utilisateurs, en ingénierie. Nos travaux récents se sont intéressés à trois facettes de la validation. La première concerne les outils pour exécuter les modèles abstraits tout au long du développement. Avec JeB [7, 9, 8], créé par F. Yang, nous pouvons observer les comportements des modèles. La deuxième concerne l’introduction progresssive et méthodique des propriétés de sécurité. Nous avons introduit des notions comme le niveau d’observation pour guider les raffinements [5, 2]. La troisième concerne l’expression des besoins et leur formalisation dans un cadre cohérent avec B-Événementiel. Les études de cas [6] ont montré le potentiel des outils comme ProR (http://wiki.event-b.org/index.php/ProR) pour lier les exigences, les modèles et les raffinements.

Sujet de doctorat et contexte du travail

La sujet proposé consiste en l’étude de la relation entre le raffinement formel, tel que défini en B-Événementiel, et la validation. Le but est de définir les conditions qui conditionnent la monotonicité de la validation par rapport au raffinement : la validation du modèle final résulterait directement de la validation de la chaîne des raffinements.

Le travail à mener peut être vu comme l’intégration des trois lignes de travaux mentionnées précédemment. La notion de scénario de validation, c’est-à-dire d’un test d’une propriété donnée, doit être le pivot du travail. Elle doit être définie autour de l’idée d’incrément de couverture des besoins associé au renforcement de l’invariant du modèle. Elle soit aussi être liée avec des éléments concrets des tests qui peuvent être conduits avec JeB.

Un élément essentiel sur lequel s’appuie notre travil de recherche pour induire et évaluer la conception d’un cadre de validation est le développement d’études de cas. Les liens étroits que le SCCH entretient avec des constructeurs d’équipements médicaux, permettent de disposer d’études de cas, réelles et complexes [4, 3], indispensables à notre approche. Des séjours régulier à Hagenberg (près de Linz) sont à prévoir au cours du travail doctoral.

Références

  • [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

Colloquium Loria 2018

Exposés précédents

Logo du CNRS
Logo Inria
Logo Université de Lorraine