Abstract
Transforming UML models into a formal representation to check certain properties has been addressed many times in the literature. However, the lack of automatic formalization for executable UML models and provision of model checking results as modeller-friendly feedback has inhibited the practical use of such approaches in real life projects. In this work we address those issues by performing the automatic formalization of the fUML (Foundational subset for executable UML) models into CSP (Communicating Sequential Processes) without any interaction with the modeller, who should be isolated from the formal methods domain. We mainly consider the formalization of systems that depend on asynchronous communication between components in order to allow checking of the dynamic concurrent behaviour of systems. We introduce also a novel approach for optimizing the generated CSP model using a group of mathematically proved optimization rules. The approach includes also providing the modeller with optimization advice for the fUML model to maximize the reduction in the state space. We design an integrated framework that handles the formalization, feedback and optimization tasks. It is implemented as a plugin to MagicDraw (the CASE tool we use) that we call Compass which depends on Epsilon as a model transformation tool that utilizes the MDE (Model Driven Engineering) approach. Compass depends on FDR2 to perform the model checking for the CSP models. In order to validate the approach and its implementation (Compass), we check three non-trivial case studies modelled in fUML. The formalization and the optimization results show the success for achieving our work objective.