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. © 2013 Springer Science+Business Media.
CITATION STYLE
Najafi, M., & Haghighi, H. (2013). An integration of UML-B and object-Z in software development process. In Lecture Notes in Electrical Engineering (Vol. 152 LNEE, pp. 633–648). https://doi.org/10.1007/978-1-4614-3535-8_53
Mendeley helps you to discover research relevant for your work.