Exigences et spécifications formelles : Patrons de développement de logiciels

Exigences et spécifications formelles : Patrons de développement de logiciels

Requirements and formal specifications : Patterns for the software development

Directrice de thèse : Mme Souquières

Professeure d’informatique à l’Université de Lorraine

Equipe DEDALE  du LORIA  (http://dedale.loria.fr)

Bureau B 205, Téléphone 03 83 59 20 12

Jeanine.Souquieres@loria.fr

Contexte. L’utilisation de méthodes formelles dans le développement de logiciels est toujours d’actualité et la question scientifique s’est déplacée. Les bases mathématiques sont raisonnablement bien comprises et les outils qui les implantent comme par exemple des démonstrateurs et des model-checkers, ont atteint une maturité suffisante pour sortir des laboratoires de recherche.  Nous savons garantir qu’une partie de programme est conforme  sa spécification.  Aujourd’hui, la question porte sur le processus et les méthodes de développement de logiciels: comment intégrer les techniques formelles? Pour cela, l’informel, ou, plus précisément, le semi-formel, et le formel doivent être pris en compte au cours du cycle de vie. Le logiciel complet est décrit par:

des textes formels. Ce sont des modèles mathématiques d’une réalité ou d’un cahier des charges lorsqu’il existe.  Par nature, ce CdC est informel; par ailleurs, un modèle doit être validé, c’est-à-dire, soumis au jugement humain ;

des textes informels. Peu de logiciels nécessitent que leur développement soit entièrement formel. Dans la réalité, seules quelques fonctions requièrent un traitement formel lourd, les autres pouvant être développées avec des techniques classiques qui ont un avantage de rapidité et de coût. La cohabitation harmonieuse de plusieurs techniques au sein d’un processus de développement est un enjeu.

Les travaux récents de l’équipe DEDALE portent sur les  outils d’aide à la validation de modèles écrits en B événementiel [4], [9]. Ils ont évolué sur la validation dès la compréhension des exigences tout au long du développement des exigences et de sa spécification formelle [6], [7]. Utilisant des techniques de transformation et de traduction au cours desquelles les développeurs introduisent des éléments  « incorrects »  au sens étroit, ces travaux ont mis en évidence la possibilité de définir des sémantiques mathématiques garantissant la correction des modèles exécutables. Ils ont aussi esquissé une extension de la notion de raffinement définie en Event-B en tant qu’étape dans le processus de développement.

Sujet de thèse.  Dans notre  approche, un processus de développement  de logiciels est défini par le triplet  <Exigences, Liens-Exigences-Spécification, Spécification>. La notion de patron a été introduite dans la programmation, avec l’approche orientée objet [2].  Son objectif est  de décrire des sous-problèmes identifiés ; une évolution de ce concept a été introduite pour décrire les spécifications formelles, notamment avec Event-B [3] en réutilisant des connaissances acquises par l’expérience. Ce sujet concerne l’introduction de patrons dans le processus de développement, c’est-à-dire qu’un patron doit prendre en compte les trois composants : les exigences, la spécification et les liens entre elles. Un patron doit gérer la vérification et la validation formelle pour obtenir des systèmes de confiance. Le travail se déroulera selon trois axes:

  • Les bases mathématiques. La définition des patrons dans le cadre de travail proposé est à préciser avec ses preuves et la vérification de ses propriétés invariantes.
  • Le processus de développement. La description et la modélisation du processus de développement est une étape indispensable vers l’intégration des activités formelles et semi-formelle. La  conception d’assistants logiciels est à envisager sur cet axe.
  • L’outillage. L’usage des méthodes formelles dépend de  manière cruciale des outils logiciels disponibles avec la plateforme Rodin (http://www.event-b.org). ProR, plug-in de Rodin, est utilisé  pour exprimer et gérer les liens entre exigences et éléments de la spécification Event-B en cours de construction.

Ce travail sera illustré par des  études de cas réelles, comme l’étude de cas du train d’atterrissage proposée à la conférence ABZ’2014 [1], ou l’étude de cas de la machine d’hémodialyse proposée à la conférence ABZ’2016 [5].

Connaissances et compétences requises.  Ce sujet se situe à la croisée de deux problématiques: la définition d’outils méthodologiques pragmatiques et les méthodes formelles. Vis-à-vis du premier courant, il convient de bien connaitre les techniques d’ingénierie logicielle. Vis-à-vis du second, il convient de maîtriser les concepts mathématiques qui permettent d’utiliser efficacement les langages de spécifications formels tels que B, Event-B. La connaissance des outils comme la plateforme Rodin, l’atelier B ou, plus généralement, les outils d’assistance à la preuve, serait appréciable.

Cadre de travail. Le travail se déroule dans le département  « Méthodes Formelles »  du LORIA avec une interaction les équipes de ce département.

Références

[1] 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.

[2] E. Gamma, R. Helm, R. Johnson, J. Vlissides. Design patterns. Elements of Reusable Object-Oriented Software. Addison Wesley, 394 pages, 1995.

[3] T. S. Hoang, A. Furst and J.-R. Abrial. Event-B Patterns and their Tool Support,  Software and System     Modeling journal, vol. 12, 2, p. 229-244, 2013.

[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] I. Sayar et J. Souquières. Du cahier des charges à la spécification. AFADL2017, Montpellier, juin 2017.

[7] I. Sayar et J. Souquières. La validation dans le Processus de Développement. Actes du 23ème Congrès INFORSID, Grenoble, France, pages 67-82, 2016. A paraître dans la Revue ISI–DAT, 25 pages, 2017.

[8] W. Su, J.-R. Abrial, Runlei Hung and Huibiao Zhu. From Requirements to Development: Methodology and Example. In Proc. Formal Methods and Software Engineering, 13th ICFEM, Durham, UK, 2011.

[9] 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.

 

En ce moment

Logo du CNRS
Logo Inria
Logo Université de Lorraine