@article{HaarmannHolfterPufahletal.2021,
  author    = {Haarmann, Stephan and Holfter, Adrian and Pufahl, Luise and Weske, Mathias},
  title     = {Formal framework for checking compliance of data-driven case management},
  series = {Journal on data semantics : JoDS},
  volume    = {10},
  journal   = {Journal on data semantics : JoDS},
  number    = {1-2},
  publisher = {Springer},
  address   = {Heidelberg},
  issn      = {1861-2032},
  doi       = {10.1007/s13740-021-00120-3},
  pages     = {143 -- 163},
  year      = {2021},
  abstract  = {Business processes are often specified in descriptive or normative models. Both types of models should adhere to internal and external regulations, such as company guidelines or laws. Employing compliance checking techniques, it is possible to verify process models against rules. While traditionally compliance checking focuses on well-structured processes, we address case management scenarios. In case management, knowledge workers drive multi-variant and adaptive processes. Our contribution is based on the fragment-based case management approach, which splits a process into a set of fragments. The fragments are synchronized through shared data but can, otherwise, be dynamically instantiated and executed. We formalize case models using Petri nets. We demonstrate the formalization for design-time and run-time compliance checking and present a proof-of-concept implementation. The application of the implemented compliance checking approach to a use case exemplifies its effectiveness while designing a case model. The empirical evaluation on a set of case models for measuring the performance of the approach shows that rules can often be checked in less than a second.},
  language  = {en}
}
@article{AwadWeidlichWeske2011,
  author    = {Awad, Ahmed Mahmoud Hany Aly and Weidlich, Matthias and Weske, Mathias},
  title     = {Visually specifying compliance rules and explaining their violations for business processes},
  series = {Journal of visual languages and computing},
  volume    = {22},
  journal   = {Journal of visual languages and computing},
  number    = {1},
  publisher = {Elsevier},
  address   = {London},
  issn      = {1045-926X},
  doi       = {10.1016/j.jvlc.2010.11.002},
  pages     = {30 -- 55},
  year      = {2011},
  abstract  = {A business process is a set of steps designed to be executed in a certain order to achieve a business value. Such processes are often driven by and documented using process models. Nowadays, process models are also applied to drive process execution. Thus, correctness of business process models is a must. Much of the work has been devoted to check general, domain-independent correctness criteria, such as soundness. However, business processes must also adhere to and show compliance with various regulations and constraints, the so-called compliance requirements. These are domain-dependent requirements. In many situations, verifying compliance on a model level is of great value, since violations can be resolved in an early stage prior to execution. However, this calls for using formal verification techniques, e.g., model checking, that are too complex for business experts to apply. In this paper, we utilize a visual language. BPMN-Q to express compliance requirements visually in a way similar to that used by business experts to build process models. Still, using a pattern based approach, each BPMN-Qgraph has a formal temporal logic expression in computational tree logic (CTL). Moreover, the user is able to express constraints, i.e., compliance rules, regarding control flow and data flow aspects. In order to provide valuable feedback to a user in case of violations, we depend on temporal logic querying approaches as well as BPMN-Q to visually highlight paths in a process model whose execution causes violations.},
  language  = {en}
}