Verification of EPC Soundness

Abstract

The aim of this book is to evaluate the power of metrics for predicting errors in business process models. In order to do so, we need to establish a clear and unambiguous understanding of which EPC business process model is correct and how it can be verify. This chapter presents verification techniques that can be applied to identify errors in EPCs with a focus on reachability graph analysis and reduction rules. Other verification techniques such as calculating invariants (see [313, 440]), reasoning (see [337, 112]) or model integration (see [403]) will not be considered.

In this chapter we will define a notion of EPC soundness for business process models (Section 3.1) and demonstrate how an analysis of the reachability graph can be applied to verify soundness of an EPC (Section 3.2). We then present a method of implementing the analysis as an extension of the EPC to Transition System plug-in for ProM. Since this verification approach suffers from the “state explosion” problem, we turn to an optimization based on a set of reduction rules (Section 3.3). For this approach we present the implementation as a batch program called xoEPC and show the results of reducing the SAP Reference model. Section 3.4 summarizes the chapter.