Taming the frame problem: an automated approach for robust UML class diagram specification and verification

It is vital to have precise specifications and verification of UML class diagrams to ensure the correctness of complex software systems. However, current specification and verification methods often face a challenge known as the frame problem. This problem occurs due to incomplete operation specifications that can lead to unintended system behavior. To tackle this issue, we have developed an automated solution to autonomously identify and define frame conditions, effectively minimizing the frame problem's impact on class diagram verification. Frame conditions are explicit contracts that meticulously outline the permissible effects of operations within the system. Our approach carefully analyzes the behavioral blueprint of a class diagram and extracts crucial information to create these conditions. Through rigorous evaluations encompassing diverse UML diagrams and simulated execution scenarios, we have demonstrated the effectiveness of our approach in preventing unintended system behavior caused by the frame problem. We have integrated the approach into the Temporal Property Validator tool, empowering practitioners to leverage its benefits for practical class diagram specification and verification.