Automatic Generation of B Specifications from 
Precise UML Notations for Data Intensive Applications






Support Tool


Our project aims at combining UML 
with the B formal method for the 
domain of database applications. It consists of 
extracting a subset of UML concepts suitable 
for the analysis of such systems, producing 
derivation rules from UML diagrams to B 
specifications and developing a prototype support tool. 
In this article, we show how formal 
specifications can be automatically generated from precise 
UML diagrams. Our study concerns the class, 
state and collaboration diagrams. This automation requires 
that the two last diagrams are annotated 
with B notations. The class diagram is 
translated into a set of B machines 
with standard update operations. Each state diagram 
is mapped into B operations to which 
proofs are attached. A collaboration diagram is 
translated into a B operation. Then the 
support tool, implemented in CAML (French version 
of ML), is presented. In order to 
build a rigorous tool, a formal UML 
metamodel has been defined and the tool 
uses an abstract syntax representation of the 
metamodel.