This paper presents a precise and descriptive semantics for core modeling concepts in Object-Z and a formal description for UML class constructs. Given the formal descriptions, it also provides a formal semantic mapping between the two languages at the meta-level, which makes our translation more systematic. Any verification of UML models can take place on their corresponding Object-Z specifications using reasoning techniques provided for Object-Z. With this approach, we provide not only a precise semantic basis for UML but also a sound mechanism for reasoning about UML models.
展开▼
