Visiting address

DS - BI
University of Groningen
Nijenborgh 9
9747 AG Groningen
The Netherlands

Quick links

Follow us

TODO

Heerko Groefsema

Research packages for the formal specification and verification of process compositions

Supervisors: Heerko Groefsema
Date: 2024-10-21
Type: bachelor-internship
Description:

For our research we implemented and use a number of Java packages that allow us to specify, unfold, and verify process compositions such as business process models and service compositions. These packages require some work, including new functionality, replacing old dependencies, adding different output formats, replacing log functionality, refactoring to use certain programming patterns, and more. In this project, we would like a number of students to improve, refactor, and add functionality. This project is available for up to 5 students, which will work on separate sub-projects such as: - Adding rich Event Log generation from random executions of annotated Petri net models. - Separating embedded data annotations and allowing execution of Petri nets using data. - Adding functionality for colored Petri nets. - Implementing improved Prime Event Structures (PES) representations of processes and unfolding (i.e., creation of PES) from Petri nets. - Replacing old dependencies and refactoring.

Conditional planning an overview of approaches

Supervisors: Heerko Groefsema
Date: 2025-02-05
Type: student-colloquium
Description:

References:
Peot, M. A., & Smith, D. E. (1992, January). Conditional nonlinear planning. In Artificial Intelligence Planning Systems (pp. 189-197). Morgan Kaufmann. Blythe, J. (1999). An overview of planning under uncertainty. Artificial intelligence today, 85-110. Rintanen, J. (1999). Constructing conditional plans by a theorem-prover. Journal of Artificial Intelligence Research, 10, 323-352. Karlsson, L. (2001, January). Conditional progressive planning under uncertainty. In IJCAI (pp. 431-438).

Verifying the data perspective of business processes

Supervisors: Heerko Groefsema
Date: 2025-02-05
Type: student-colloquium
Description:

References:
Groefsema, H., Beest, N.R.T.P.v., Governatori, G. (2022). On the Use of the Conformance and Compliance Keywords During Verification of Business Processes. In: Business Process Management Forum. BPM 2022. Lecture Notes in Business Information Processing, vol 458. Springer. H. Groefsema, N.R.T.P. van Beest, A. Armas-Cervantes, Efficient conditional compliance checking of business process models, Computers in Industry, Volume 115, 2020. Alin Deutsch, Richard Hull, Fabio Patrizi, and Victor Vianu. 2009. Automatic verification of data-centric business processes. In Proceedings of the 12th International Conference on Database Theory (ICDT '09). N. van Beest, H. Groefsema, A. Cryer, G. Governatori, S. C. Tosatto and H. Burke, Cross-Instance Regulatory Compliance Checking of Business Process Event Logs, in IEEE Transactions on Software Engineering, vol. 49, no. 11, pp. 4917-4931, Nov. 2023.

Model Checking for Environmental Sustainability

Supervisors: Heerko Groefsema, Michel Medema
Date: 2025-12-05
Type: bachelor-project/master-project
Description:

Organisations are increasingly concerned with environmental sustainability for various reasons (e.g., legislative, economic, ecological, or social). Quantifying sustainability performance across different dimensions is necessary for fulfilling legislative requirements and evaluating improvement efforts. In this project you will extend existing model checking approaches so that they can deal with business process models in which key environmental indicators have been attached to tasks and subprocesses along with possible target values for those indicators that should be enforced during process execution.

Runtime Compliance Checking for Camunda 8

Supervisors: Heerko Groefsema, Michel Medema
Date: 2025-12-05
Type: bachelor-project/master-internship/master-project
Description:

Organisations are increasingly concerned with environmental sustainability for various reasons (e.g., legislative, economic, ecological, or social). Quantifying sustainability performance across different dimensions is necessary for fulfilling legislative requirements and evaluating improvement efforts. In this project you will integrate an existing compliance checking tool into the Camunda 8 platform.

Verification of Security and Privacy concepts in BPMN Choreography diagrams

Supervisors: Heerko Groefsema
Date: 2025-12-05
Type: bachelor-project/master-project
Description:

Where process models define the flow of activities of participants, choreographies describe interactions between participants. Within such interactions, the security and privacy related concepts of separation of duties and division of knowledge are important. The former specifies that no one person has the privileges to misuse the system, either by error or fraudulent behavior, while the latter defines the absence of total knowledge within a single person, such that the knowledge can not be abused. The problem is, how do we specify such concepts and what kind of model is required to verify these concepts? In this project we ask the student to devise an approach to formally specify and verify these concepts given a BPMN Choreography Diagram.
References:
OMG. Business process model and notation (BPMN) version 2.0, 2011. Pullonen, Pille & Matulevičius, Raimundas & Bogdanov, Dan. (2017). PE-BPMN: Privacy-Enhanced Business Process Model and Notation. 40-56. BPMVerification package

Obtaining Alignments from Transition Graphs

Supervisors: Heerko Groefsema
Date: 2025-12-05
Type: bachelor-project/master-project
Description:

The practice of checking conformance of business process models has revolutionized the industry through the amount of insight it creates into the process flows of businesses. Conformance checking entails matching an event log (which details events of past executions) against a business process model (which details the prescribed process flow) through a so called alignment. Any deviation from the prescribed process flow is detected and reported. Generally, alignments are obtained by matching the so called token replay of process models (e.g., Petri nets) against events in logs. Our Transition Graphs are also obtained from token replays, but offer further insight into parallel executions than regular Reachability Graphs. As a result, we are interested in the applicability of obtaining alignments using Transition Graphs, especially when matched against event logs that include lifecycle events and thus offer parallel execution data. In this project we ask the student to implement and evaluate the applicability of such an approach.
References:
H. Groefsema, N.R.T.P. van Beest, and M. Aiello (2016) A Formal Model for Compliance Verification of Service Compositions. IEEE Transactions on Service Computing. Carmona, Josep, et al. "Conformance checking." Switzerland: Springer.[Google Scholar] (2018). BPMVerification package

Obtaining Alignments from behavior

Supervisors: Heerko Groefsema
Date: 2025-12-05
Type: master-project
Description:

The practice of checking conformance of business process models has revolutionized the industry through the amount of insight it creates into the process flows of businesses. Conformance checking entails matching an event log (which details events of past executions) against a business process model (which details the prescribed process flow) through a so called alignment. Any deviation from the prescribed process flow is detected and reported. Generally, alignments are obtained by matching the so called token replay of process models (e.g., Petri nets) against events in logs. Instead, we would like to investigate comparing event logs against a specification of ordering relations to achieve a significant performance increase.