Transformation systématique de spécifications UML en B

Rapport interne.La dérivation de spécifications UML en B est considérée comme une approche appropriée afin d'utiliser conjointement UML et B dans un développement unifié, pratique et 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. Cet article présente une procédure de dérivation d'une spécification B à partir d'un ensemble de diagrammes UML de classes et de collaboration. Cette procédure est basée sur une approche utilisant le raffinement B pour modéliser les opérations UML. La procédure de dérivation est complétée par un ensemble de schémas de dérivation d'OCL en B. Ce qui permet de compléter la transformation des modèles UML en B en prenant en compte des contraintes OCL associées aux diagrammes UML: les invariants de classes, les pré-et postconditions des opérations, les gardes au sein des diagrammes de collaboration