Formal redesign of UML class diagrams

Abstract

In this paper we study a formal concept of redesign for object-oriented specifications. This concept corresponds to the UML notion of abstraction. The notion of refinement, which has been extensively studied also at the formal level, models well incremental approach where new requirements are added, but can not be changed. This assumption is usually not satisfied in software engineering process where permanent change is a constant factor. We study therefore a new notion which generalizes the notion of interpretation used in algebra. This notion is very flexible and allows us for comparison of different class diagrams even if one of them contains requirements excluded by another. To compare specifications, we map model elements in the first specification on the related model elements in the second specification. This mapping defines a UML trace; it can be lifted to the level of OCL as well as to the level of first order logic and then extended to an interpretation function. We also provide a formal foundation for our concepts and prove its soundness. We demonstrate the applicability of our approach in a series of examples.