Visual and formal modeling notations can complement each other when developing software systems. Object-Z (OZ) is an object-oriented extension of the Z notation for writing formal specifications. Much work exists on translations between UML and OZ. However, UML is not a formal modeling language. This delays verification and validation of UML visual models until translation to OZ. On the other hand, UML-B is a UML-like formal modeling language that supports object-oriented modeling concepts. In this paper, we propose a formal mapping from UML-B models to OZ constructs in order to integrate these two object-oriented visual and non-visual formal notations. In this way, we assist the software development process by using UML-B as a visual modeling notation at early conceptual modeling stage and OZ at next stages when requirements are better understood. Also, an opportunity is provided to develop code from UML-B models using existing approaches for mapping OZ specifications to object-oriented programs. Finally, using UML-B instead of UML, we are able to verify visual models in the early conceptual modeling stage of the software development process without translating them into OZ specifications.
展开▼
