Approche formelle pour la dérivation de vues structurelles UML à partir de développements B. Formalisation, preuve et extension pour la prise en compte des raffinements B
Les méthodes formelles sont aujourd'hui l'un des moyens les plus rigoureux pour développer des logiciels ou modéliser des systèmes. Cependant, la complexité de leurs notations constitue un frein à leur adoption. En effet, les spécifications qui en résultent restent difficiles à lire quand elles ne sont pas accompagnées d'une bonne documentation. Dans le cadre de nos travaux antérieurs nous avons proposé un environnement de retro-ingénierie permettant de documenter graphiquement des spécifications B en en dérivant automatiquement des vues structurelles UML. Dans cet article, nous présentons une formalisation en B de notre technique et nous prouvons que les modèles générés répondent bien à des critères de pertinence. Finalement, nous montrons comment notre travail peut être appliqué sur des raffinements B.
Formal methods are nowadays one of the most rigorous ways to develop software and model systems. But their notations are complex which prevents their adoption. In fact, formal models remain difficult to read when they are not well documented. In a previous work we proposed a reverse-engineering framework which allows to graphically document B specifications by automatically deriving structural UML views. Our approach is based on a concept formation technique. In this paper, we formalize our algorithm and we prove that the generated context models satisfy a set of pertinency criteria. Finally, we show how our technique can be used in order to take refinements into account.
A.IDANI, Y.LEDRU, D.BERT
Reçu le 13 avril 2006.
Accepté le 18 janvier 2007.
méthode B, UML, analyse formelle de concepts, intégration de méthodes.
B method, UML, formal concept analysis, method integration.
Français
|
