Frame conditions in the automatic validation and verification of UML/OCL models: A symbolic formulation of modifies only statements

Validation and verification of UML/OCL models is a crucial task in the design of complex software/hardware systems. The behavior in those models is expressed in terms of operations with pre- and postconditions. These, however, are often not precise enough to describe what may or may not be modified in a transition between two system states. This frame problem is commonly addressed by providing additional constraints in terms of so-called frame conditions and has already been considered in different research areas in the last decades—except for UML/OCL where corresponding approaches have been investigated only recently. Among these, the so-called modifies only statements constitute a very promising concept which is complementary to all other approaches. More precisely, instead of allowing arbitrary modifications in principle and prohibiting certain undesired behavior, the statements explicitly describe what is allowed to change. However, this approach to frame conditions has not been considered so far in any of the numerous approaches for the automatic validation and verification of the behavior in UML/OCL models that have been proposed in the last years. Most of these approaches rely on a symbolic formulation of all possible system states and transitions between them. Therefore, in this paper we explain how modifies only statements can be integrated into an existing symbolic formulation. Based on this, we evaluate the applicability of the presented concept and compare it to previous implementations of frame conditions.