A CSP Semantics for UML State Machines Aiming at Hidden Formal Methods Verification

• Diego Ferreira UFRPE
• Lucas Lima UFRPE

Resumo

The increasing complexity of software systems, especially in safety-critical domains, requires rigorous verification methodologies to ensure reliability and correctness. This paper presents a semantics for UML state machines using the formal language CSP to support automatic property verification. Our approach integrates the intuitive modeling capabilities of UML with the precise verification tooling available for CSP, thus facilitating the detection and correction of design errors at the early stages of system development. We implemented a framework as a plugin for the Astah modeling tool, which translates UML diagrams into CSP specifications and utilizes the FDR model checker for verification. The results are traced back to the diagram level, thus hiding the complexity of formal notations and tools. A case study of a flashlight system demonstrates the practical applicability and benefits of our approach, highlighting its ability to identify and solve design issues early in the development process.