Model Checking to support Action Controls in the Purchasing Process

In this paper, we use model checking to perform the analysis and the assessment of the Purchasing Process performance in the field of Action Controls. The aim of these controls, in a Management Control Systems, is to ensure that the employee behaviours are consistent with the objectives and strategies of the organization. However, model checking suffers from the so-called 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: (i) we show how model checking can be applied in the context of business process modelling and analysis, (ii) we evaluate and test the reduction methodology using an academic case study. Our investigations suggest that the business community can benefit from this efficient methodology developed in formal methods since it can detect errors that were missed by traditional verification techniques. Thus, formal methods can be adopted to enhance the effectiveness of the organizational control together with an increase of process efficiency levels. We show and discuss the obtained experimental results.