An Optimization Approach for Effective Formalized fUML Model Checking

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 effective 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 first 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 effectiveness 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.