B/UML (Mise en relation de spécifications B et de descriptions UML pour l'aide à la validation externe de développements formels en B)

Les exigences qui s'appliquent aux composants logiciels et aux logiciels embarqués justifient l'utilisation des meilleures techniques disponibles pour garantir la qualité des spécifications et conserver cette qualité lors du développement du code. Les méthodes formelles, et parmi elles la méthode B, permettent d'atteindre ce niveau de qualité. Cependant, ces méthodes utilisent des notations et des concepts spécifiques, qui génèrent souvent une faible lisibilité et une difficulté d'intégration dans les processus de développement et de certification. Ainsi, proposer des environnements de spécification, de développement de programmes et de logiciels, combinant des méthodes formelles et des méthodes semi-formelles largement utilisées dans les projets industriels, en l'occurrence B et UML, s'avère d'une grande importance. Notre intérêt porte précisément sur la méthode B qui est une méthode formelle utilisée pour modéliser des systèmes et prouver l'exactitude de leur conception par raffinements successifs. Mais les spécifications formelles sont difficiles à lire quand elles ne sont pas accompagnées d'une documentation. Cette lisibilité est essentielle pour une bonne compréhension de la spécification, notamment dans des phases de validation ou de certification. Aujourd'hui, en B, cette documentation est fournie sous forme de texte, avec, quelquefois, des schémas explicitant certaines caractéristiques du système. L'objectif de ce travail de thèse est de mettre en relation des spécifications en B avec des diagrammes UML, qui constituent un standard de facto dans le monde industriel et dont le caractère graphique améliore la lisibilité. Nous avons axé notre processus de dérivation de diagrammes de classes à partir de spécifications B autour d'une technique d'ingénierie inverse guidée par un ensemble de correspondances structurelles et sémantiques spécifiées à un méta-niveau. Quant à la dérivation de diagrammes d'états/transitions, elle a été orientée vers une technique d'abstraction de graphes d'accessibilité construits par une exploration exhaustive du comportement de la spécification.GRENOBLE1-BU Sciences (384212103) / SudocSudocFranceF