Application of Equivalence Checking in a Loan Application & Verification

Application of Equivalence Checking in a Loan Application & Verification

Equivalence checking is traditionally applied to computer system design. It is a promising formal technique for the improvement of software quality. However, it requires detailed specifications of systems and is therefore not very accessible, above all in certain restricted fields of application. One of this domain is business process management. In particular, we examine the applicability of equivalence checking to validation of Business Processes that are mapped through the systems of Workflow Management. The usage of formal methods in business domain, however, is still not widely used. This is due also to the state explosion problem, which says that the state space grows exponentially in the number of concurrent processes. In this paper we consider a heuristic-based methodology developed to combat the state explosion problem for checking process equivalence. Our proposal is two-fold: (i) we show how equivalence checking can be applied in the context of business modelling and analysis; (ii) we evaluate and test the heuristic-based methodology using, as a case study, a real-world banking workflow of a loan origination process. Our investigations suggest that the business community, especially in the banking held, can benefit from this efficient methodology developed in the process algebra area to prevent significant errors. We show and discuss the experimental results obtained.

Formal methods are powerful techniques for specifying and verifying complex systems. Several techniques for formal verification have been developed over the past three decade among them equivalence checking. Equivalence checking is the process of determining whether two systems are equivalent to each other according to some mathematically-defined notion of equivalence. Equivalence checking is typically used to verify if a system design conforms to its high-level service
specification. Although equivalence checking is currently not applicable to all domains, it is useful for certain restricted fields of application. One of this domain is business process management. In particular, we examine the applicability of equivalence checking to validation of Business Processes that
are mapped through the systems of Workflow Management. The usage of this formal method in the domain of business process management however, is still not widely used.

In fact, the parallelism between the processes of the system leads to a number of reachable states which may become very large, in some cases on the order of millions or billions of states. When the number of states is too large to fit in a computer’s main memory, verification quickly breaks down. In fact, in the business process taken into account, we came across the state explosion problem. Specifically, this problem has emerged as a result of a first modelling of the banking process, in which the excessive number of processes in parallel has made impracticable the verification
using standard model checker

Several approaches have been developed to solve or reduce the state explosion problem. In this paper to combat the state explosion problem for checking process equivalence we consider an efficient procedure, based on heuristic search [1], proposed in [2]. The procedure is applied to processes defined through a specification language very compact, the Calculus of Communicating Systems (CCS)[3] defined by Milner, which is one of the most well known process algebras and it is largely used for modeling concurrent and distributed systems. The approach uses a heuristic function that suggests to expand
first the states that offer the most promising way to deduce that two systems are not equivalent. This makes it possible to avoid the exhaustive exploration of the global state graph of the two systems when they are not equivalent. One of the authors of this paper has contributed to the design of
Grease (GREedy Algorithm for System Equivalence), a C++ tool supporting the heuristic approach to check equivalence of CCS processes. The use of Grease on a sample of small CCS processes has shown a significant reduction of both state-space size and time, compared to traditional equivalence
checking algorithms. Our proposal is two-fold: (i) we show how equivalence checking can be applied in the context of business modelling and analysis; (ii) we evaluate and test the heuristic-based methodology using, as a case study, a real- world banking workflow of a loan origination process

In this section we introduce the basic concepts of formal methods. Formal methods are mathematically based languages, techniques, and tools for specifying and verifying complex systems. Several techniques for formal verification have been developed over the past three decade among them equivalence
checking.

As stated above, the application of formal techniques con-sists of an algorithmic approach to verification of such systems that can be represented by a formal model. According to the mentioned outlook, these methodologies are primarily related to verification of hardware and software systems. However,
formal techniques and tools have a number of features that make it possible to extend their use to specific business domains, including the formal verification of business pro- cesses that are mapped and administrated through the systems of Workflow Management. The latter are generally used by
managers to automate all or part of business processes by flushing documents, information and tasks from one participant to another, according to a set of procedural rules. With specific reference to dynamic workflows