Coupling-based transformations of Z specifications into UML diagrams

Due to their accuracy in describing systems, formal specifications can play an important role during forward as well as reverse engineering activities. However, besides dense mathematical expressions, their lack in visually appealing notations impedes their use and exchange among different stakeholders. One solution to this problem is to enrich the specification by other views, in most cases Unified Modelling Language (UML) diagrams. But the mapping is not trivial, and existing approaches have their impediments, among them the assignment of methods to classes—which has to be re-done by hand quite often. By the example of Z, this paper demonstrates that the situation can be improved. The new approach combines existing mapping strategies, but additionally lets the assignment of methods rest on quality-related measures. The basic idea is to balance the values of coupling for all methods within and between the UML classes. With that, two issues are addressed: firstly, the mapping of sets, types, and operations (to UML classes and UML methods) is based on reproducible measures that are intuitively comprehensible. Secondly, implementations based on the resulting UML class diagrams very likely also have comparable quality-related properties.