B formal modeling based on UML class

We chose class diagram as the UML model to be formalized by B specification, building the domain model to extract metaclass as a basic unit. According to the source of attributes, we classify them into inline attribute and associated attribute, and discuss the formal methods under different situations. Analyze association, the construction of associated class, and their formal methods. Comparing the class operation and the operation of abstract machine, we put forward the layered methods to formalize the operation. At last, we show the layered structure of formalization for UML static model.