Counterexample Analysis for Supporting Containment Checking of Business Process Models

During the development of a process-aware information system, there might exist multiple process models that describe the system’s behavior at different levels of abstraction. Thus, containment checking is important for detecting unwanted deviations of process models to ensure a refined low-level model still conforms to its high-level counterpart. In our earlier work, we have interpreted the containment checking problem as a model checking problem and leveraged existing powerful model checkers for this purpose. The model checker will detect any discordance of the input models and yield corresponding counterexamples. The counterexamples, however, are often difficult for developers with limited knowledge of the underlying formal methods to understand. In this paper, we present an approach for interpreting the outcomes of containment checking of process models. Our approach aims to analyze the input models and counterexamples to identify the actual causes of containment inconsistencies. Based on the analysis, we can suggest a set of countermeasures to resolve the inconsistencies. The analysis results and countermeasures are visually presented along with the involved model elements such that the developers can easily understand and fix the problems.