Traduction systématique de spécifications
Institution:
Nancy 2Disciplines:
Directors:
Abstract EN:
The diversion of the specifications UML towards B is considered as an approach suited to use jointly UML and B in a unified, practical, rigorous development of software. On one hand, this diversion allows to use the specifications UML as starting point to develop the specifications B. On the other hand, it is possible to use tools powerful supports(media) of B as AtelierB to analyze the specifications B diverted to identify the defects within specifications UML. This thesis(theory) concentrated on the diversion towards B for the diagrams of interaction (collaboration, sequence), the diagrams of state-transition and the diagrams of case of use, which was not previously considered. Three procedures of diversion for three types of behavioral diagrams were proposed. Furthermore, the plans of diversion of the constraints OCL towards B were defined. Which allows to divert systematically towards B not only the invariants of classes in OCL, the conditins of guards (always in OCL) within the diagrams of state-transition but also the specifications OCL of the pre-form and postcondition from concepts UML behavioral as operations UML, cases of use and from the events. We also developed a tool of support for the diversion of UML / OCL towards B. Besides the plans of diversion of UML / OCL towards B, we proposed certain analyses of coherence, thanks to B and its tools, within the specification UML have. This thesis can be pursuit
Abstract FR:
La dérivation des spécifications UML vers B est considérée comme une approche appropriée afin d'utiliser conjointement UML et B dans un développement unifié, pratique, rigoureux de logiciels. D'une part, cette dérivation permet d'utiliser les spécifications UML comme point de départ pour développer les spécifications B. D'autre part, il est possible d'utiliser les outils supports puissants de B comme AtelierB pour analyser les spécifications B dérivées afin d'identifier les défauts au sein de spécifications UML. Cette thèse s'est concentrée sur la dérivation vers B pour les diagrammes d'interaction (collaboration, séquence), les diagrammes d'état-transition et les diagrammes de cas d'utilisation, qui n'a pas été considérée précédemment. Trois procédures de dérivation pour trois types de diagrammes comportementaux ont été proposées. De plus, les schémas de dérivation des contraintes OCL vers B ont été définis. Ce qui permet de dériver systématiquement vers B non seulement les invariants de classes en OCL, les conditins de gardes (toujours en OCL) au sein des diagrammes d'état-transition mais aussi les spécifications OCL de la forme pré- et postcondition des concepts UML comportementaux comme des opérations UML, des cas d'utilisation et des événements. Nous avons aussi développé un outil de support pour la dérivation d'UML/OCL vers B. En plus des schémas de dérivation d'UML/OCL vers B, nous avons proposé certaines analyses de cohérence, grâce à B et ses outils, au sein de la spécification UML ont. Cette thèse peut être poursuite par l'utilisation des schémas de dérivation sur les études de cas réelles afin d'évaluer leur application. Une autre voie est de définir des schémas de dérivation de B vers UML