Verifying deadlock and nondeterminism of UML/SysML state machines integrated with activities

Abstract

This paper presents a framework for verifying deadlock and nondeterminism in UML/SysML state machines integrated with activities, addressing the critical need for automated checks in UML projects. The framework aims to provide architects and system designers with na automated way to model and verify properties in state machine diagrams integrated with activity diagrams, emphasizing the absence of deadlock and nondeterminism crucial aspects in critical systems. The framework is implemented as a plug-in for the Astah modeling environment, utilizing the Astah API to read the components used in state machine and activity diagrams. The translation of the diagram is performed into the formal CSP language and is verified using the FDR tool. In the case of deadlock or nondeterminism, an interactive counterexample is generated in the modeling platform, facilitating the identification of the reasons for the failure. 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 highlights the limitations and future directions for the framework.