Automatic generation of object-Z specification from UML diagrams

High quality software requirement specification is crucial for software development. Although efforts and research works have been devoted to address the problem, the errors in user requirement still hinder us from development high quality software. Formal methods have been proposed as the one of the most promising solutions to the problem. But formal specification is difficult to create. One recent trend in the software requirement engineering research field is to integrate UML with a suitable formal notation. The UML/OCL notation offers a standard language for system modeling. However, the current lack of formal semantics for UML/OCL makes it hard to validate and verify UML models. And formal methods provide mature tools for validation and verification. In this paper, we propose an approach to transforming class and statechart diagrams, as well as OCL constraints into Object-Z specification and design an automated tool UMLFormalzier to support our approach.