TGG-based process for automating the transformation of UML models towards B specifications

摘要

The UML notation provides a standard framework for the purpose of object modelling by several diagrams (classes, statecharts, etc.). These, form confirmed advantages: re-use of components, high level of abstraction, semantic richness, graphic and synthetic view. Nevertheless, the object-oriented notations lack of formalisation and miss of reliable bases for the analysis and verification of the applications. To overcome this problem, we suggest a solution to the UML graph transformation towards formal methods, in particular the B method. The goal of this paper is to automate the generation of B language, starting from UML class and statechart diagrams by mean of graph grammar rules. This automation is achieved by the tool TGG Interpreter. The major advantage of this transformation: it is a declarative; visual; and formal approach to handle graphs. A lift control system is developed to illustrate our study.