What is Model Checking

Traditional business process specification approaches such as BPMN are procedural, as they require specifying exact and complete process flow. In contrast, a declarative process is specified by a set of constraints that mark the boundary of any solution to the process. In this chapter, the authors propose a bounded model-checking-based approach for the verification of declarative processes using satisfiability solving (SAT). The proposed approach does not require exponential space and is very efficient. It uses the highly expressive event calculus (EC) as the modeling formalism, with a sound and complete EC to SAT encoding process. The verification process can include both the functional and non-functional aspects. The authors have also proposed a filtering criterion to filter the clauses of interest from the large set of unsatisfiable clauses for complex processes. The authors have discussed the implementation details and performance evaluation results to justify the practicality of the proposed approach.