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.Butformal 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.
UML Object- Z formalization method integration UMLFormalizer
MIAO Huaikou CHEN Yihai
School of Computer Engineering and Science Shanghai University 149 Yanchang Road, 200072, Shanghai, School of Computer Engineering and Science Shanghai University 149 Yanchang Road, 200072,,Shanghai,
国际会议
厦门
英文
857-862
2006-07-27（万方平台首次上网日期，不代表论文的发表时间）