Generation and validation of frame conditions in formal models

Operation contracts are a popular description means in behavioral system modeling. Pre- and postconditions are used to describe the effects on model elements (such as attributes, links, etc.) that are enforced by an operation. However, it is usually not clearly stated what model elements may be affected by an operation call and what shall remain unchanged—although this information is essential in order to obtain a comprehensive description. A promising solution to this so-called frame problem is to define additional frame conditions. However, properly defining frame conditions which complete the model description in the intended way can be a non-trivial, tedious, and error-prone task. While in general there are several tools and methods for obtaining formal model descriptions and also a broad variety of approaches for the validation and verification of the generated models, corresponding methods for frame conditions have not received significant attention so far. In this work, we provide a comprehensive overview of recently proposed approaches that close this gap and support the designer in generating and validating frame conditions.