Verifying Integrated Designs of UML State Machines and Activities Using CSP

This paper presents a framework for verifying deadlock and nondeterminism in UML state machines integrated with activities, addressing the critical need for automated checks in UML projects. The framework aims to support architects and system designers in modeling and verifying properties of state machine diagrams integrated with activity diagrams, emphasizing the absence of deadlock and nondeterminism, crucial aspects of critical systems. We implemented this tool as a plug-in for the Astah modeling environment, utilizing the Astah API to read the components used in state machine and activity diagrams. We consider the formal language CSP as the underlying semantic domain, and we verify the translated models using the FDR tool. In the case of an issue is found, an interactive counterexample is generated in the modeling platform, facilitating the identification of the reasons for the failure and to hide the complexity of the rigorous notation and manipulation of formal method tooling. The paper also discusses the developed semantics, a case study, and the functionalities of the framework. Additionally, it compares this work with related approaches and discusses its limitations and future directions.