Checking Compliance in Data-Driven Case Management

Case management approaches address the special requirements of knowledge workers. In fragment-based case management (fCM), small structured parts are modelled and loosely coupled through data dependencies, which can be freely combined at run-time. When executing business processes, organizations must adhere to regulations, to laws, to company guidelines etc. Business process compliance comprises methods to verify designed and executed business processes against certain rules. While design-time compliance checking works well for structured process models, flexible knowledge-intensive processes have been rarely considered despite increasing interest in academia and industry. In this paper, we present (i) formal execution semantics of fCM models using Petri nets. We also cover concurrently running fragment instances and case termination. We (ii) apply model checking to investigate the compliance with temporal logic rules; finally, we (iii) provide an implementation based on the open-source case modeler Gryphon and the free model checker LoLA.