Automatically formalizing fUML models into CSP is a challenging 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 communication 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 explosion 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 approach, we design a framework that works on two levels; the first one provides optimization advice to the modeller, while the second one automatically applies optimization rules which transform the CSP model to a more optimized one with a reduced state space. Implementing and applying the approach on two large case studies demonstrated the effectiveness of the approach. We also prove that the optimization rules are safe to be applied automatically without eliminating important information from the CSP model.
展开▼
