FormalizedfUMLModelChecking.PDFVIP

An Optimization Approach for E?ective Formalized fUML Model Checking Islam Abdelhalim, Steve Schneider and Helen Treharne Department of Computing, University of Surrey i.abdelhalim, s.schneider, h.treharne @ surrey.ac.uk Abstract. Automatically formalizing fUML models into CSP is a chal- lenging task. However, checking the generated CSP model using FDR2 is far more challenging. That is because the generated CSP model holds many implementation details inherited from the fUML model, as well as the formalization of the non-trivial fUML inter-object communica- tion mechanism. Using the state space compression techniques available in FDR2 (such as Supercompilation and compression functions) is not enough to provide an e?ective model checking that avoids the state ex- plosion problem. In this paper we introduce a novel approach that makes use of a restricted CSP model (because it follows certain formalization rules) to optimize the generated model. As an application of our ap- proach, we design a framework that works on two levels; the ?rst one provides optimization advice to the modeller, while the second one au- tomatically applies optimization rules which transform the CSP model to a more optimized one. Implementing and applying the approach on two large case studies demon- strated the e?ectiveness of the approach. We also proved that the opti- mization rules are safe to be applied automatically without eliminating important information from the CSP model. 1 Introduction Formalizing fUML (Foundational Subset for Executable UML) [1] models to a CSP (Communication Sequential Processes) [2] formal representation, has been previously considered [3, 4]. Having many implementation details in the fUML models and considering the asynchronous inter-object communication mecha- nism of t