Automated Mitigation of Frame Problem in UML Class Diagram Verification

The validation and verification of UML class diagrams are essential for ensuring the correctness of complex software systems. However, existing approaches have limitations, such as the inability to automatically deal with the frame problem. The frame problem occurs when operation specifications are incomplete, which can lead to unintended system behavior. This paper proposes an automated approach to specify frame conditions for class diagram verification. Frame conditions are operation contracts that explicitly define the effects an operation may have on the system to mitigate the frame problem. The proposed approach analyzes the behavioral specification of a class diagram to identify relevant information and specify frame conditions. To evaluate the approach, we used the approach to automatically specify frame conditions for different UML diagrams. We then simulated different execution scenarios and analyzed them to evaluate the effectiveness of the specified frame conditions in preventing unintended system behavior resulting from the frame problem. The approach has been implemented and put into practice in the Temporal Property Validator (TPV) tool.