Efficient formal verification in banking processes

Model checking is a very useful method to verify concurrent and distributed systems which is traditionally applied to computer system design. We examine the applicability of model checking to validation of Business Processes that are mapped through the systems of Workflow Management. The use of model checking in business domain is affected by the state explosion problem, which says that the state space grows exponentially in the number of concurrent processes. In this paper we consider a property-based methodology developed to combat the state explosion problem. Our focus is two fold; firstly we show how model checking can be applied in the context of business modelling and analysis and secondly we evaluate and test the 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 field, can benefit from this efficient methodology developed in formal methods since it can detect errors that were missed by traditional verification techniques, and being cost-efficient, it can be adopted as a standard quality assurance procedure. We show and discuss the experimental results obtained