Powerful Equivalence Checking in the Bank Supply Process

摘要

Equivalence checking is a powerful formal technique to improve the quality of computer and software systems. It is usually employed to verify the correctness in a model-based design. Notwithstanding, a detailed and precise specification is required in order to apply equivalence checking to a given domain. Unfortunately, certain fields of application like business process management lack of such adequate information. We explore the applicability of equivalence checking to validation of Business Processes described by the aid of Workflow Management systems. Due to the state explosion problem, formal methods are not very popular in the business domain. In fact, the state space grows exponentially in the number of concurrent processes leading to an impracticable verification. In this paper we deal with a heuristic-based methodology developed to beat the state explosion problem when checking non-equivalence. Our contribution is two-fold: (i) we show how equivalence checking can successfully operate in the business modelling and analysis context, (ii) we model and use the bank supply process as a real case study to evaluate and test the heuristic-based methodology. We show and debate encouraging experimental results comparing them with a state of the art model checker i.e. CADP. This suggests that the business community, mostly in the banking field, can take advantage from our efficient methodology based on process algebra.