Lima, Lucas Albertins deFerreira, Diego Soares Pires2025-08-152024-02-20FERREIRA, Diego Soares Pires. Verifying deadlock and nondeterminism of UML/SysML state machines integrated with activities. 2024. 20 f. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação) – Departamento de Computação, Universidade Federal Rural de Pernambuco, Recife, 2024.https://arandu.ufrpe.br/handle/123456789/7517This 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.20 f.en-USopenAccesshttp://creativecommons.org/licenses/by-nd/4.0/State machineActivityDeadlockNondeterminismCSP (Computer program language)bachelorThesisAttribution-NoDerivatives 4.0 International