Heerko Groefsema

PhD in Computer Science

Heerko is a post-doctoral researcher at the Distributed Systems group of the University of Groningen, the Netherlands. He received the Ba. in information and communication technology at the Hanzehogeschool Groningen in 2004, and the B.Sc. and M.Sc. in computer science at the University of Groningen in 2006 and 2008, respectively. He successfully defended his thesis Business Process Variability: a Study into Process Management and Verification at the University of Groningen in 2016. His research interests include business process and service composition compliance, verification, and variability.

University of Groningen, Nijenborgh 9, 9747 AG Groningen, The Netherlands

Bernoulliborg room 591 (Tue & Thu 10:00 -- 15:00)

h.groefsema [at] rug.nl



Business Process Variability

A study into Process Management and Verification

Business Process Management (BPM) manages and optimizes business processes with the intent to increase productivity and performance. BPM is a rapidly evolving field due to new requirements emerging at agile branches of business where business processes are required to be less and less rigid. Where BPM supported local user-specific rigid and repetitive units of work in the past, these days it is required to support loosely-coupled processes in cloud configurations among many users with each many different requirements.

As the field of BPM continues to manage an increasing number of rapidly evolving business processes in agile environments, the evolution of each business process must continue to always behave in a correct manner and remain compliant with the laws, regulations, and internal business requirements imposed upon it. To manage the correct behavior of quickly evolving business processes, or the definition of a wide variety of similar business processes, we evaluate the application of formal verification techniques as a possible solution for the pre-runtime analysis of the correct behavior and compliant design of business processes within possible process families.

A novel approach allowing pre-runtime verification that supports the different branching and merging constructs allowed by business process models and their service compositions is presented. Evaluations on expressive power demonstrate that, other than the generally employed transition systems, the proposed model correctly captures well-known business process patterns. Furthermore, it maintains information on parallel occurrences of activities and the local next activity occurrence: an ability which is unique to the presented approach.


Automated compliance verification of business processes in Apromore (, and ), In Proceedings of the BPM Demo Track 2017, .

A Formal Model for Compliance Verification of Service Compositions (, and ), In IEEE Transactions on Service Computing, IEEE, .

Business Process Variability: A Study into Process Management and Verification (), Rijksuniversiteit Groningen, . [pdf]

Design-time Compliance of Service Compositions in Dynamic Service Environments ( and ), In IEEE International Conference on Service Oriented Computing & Applications, . [pdf]

A Survey of Formal Business Process Verification: From Soundness to Variability ( and ), In International Symposium on Business Modeling and Software Design, . [pdf]

Imperative versus Declarative Process Variability: Why Choose? ( and ), Technical report JBI 2011-12-6, University of Groningen, . [pdf]

Business Process Variability: A Tool for Declarative Template Design ( and ), In International Conference on Service-Oriented Computing - Demo Track, .

Declarative Enhancement Framework for Business Processes ( and ), In International Conference on Service-Oriented Computing, . [pdf]

Requirements and Tools for Variability Management (), In IEEE Workshop on Requirement Engineering for Services at IEEE COMPSAC, . [pdf]


BPM Verification Package

The business process verification package provides generic verification tools for Petri net based business process models. A version of this package has been implemented in the Apromore Advanced Process Analytics Platform. The package provides the following functionality:

  • Generation of a declarative process specification describing the common behavior of one or more related pnml process model variants.
  • Verification of a pnml process model against a generated or custom specification using the NuSMV2/NuXMV model checker.


The Verification extension for Business Process Modeling Tool (VxBPM) is a business process modeling tool which provides control flow verification of business process models. The tool is written using the Java programming language and features

  • BPMN BPD design abilities,
  • Saving and loading to XPDL format,
  • Automated pattern-based model transformation to CPN,
  • Automated generation of the Kripke structures required for verification,
  • Automated verification using one of multiple model checkers, and
  • Transparent visual and textual feedback of the generated models and verification results.


The ProVariant tool allows for the automated generation of declarative specifications from a set of known business process variants. It takes as input a set of process models in PNML format. Its output is a set of CTL specifications.


Journal Review Invitations:

  • IEEE Transactions on Services Computing
  • Elsevier's Computers in Industry
  • Springer's International Journal on Software Tools for Technology Transfer

Programme Committee Memberships:

  • APPIS 2018
  • ESOCC 2017
  • ESOCC 2016

Sub-review Invitations:

  • ICWS 2017
  • WISE 2015
  • SOCA 2015
  • OPODIS 2014
  • Cloud 2014
  • CoopIS 2013
  • ICWS 2013
  • Cloud 2012
  • Cloud 2011
  • ICWS 2011
  • CoopIS 2010
  • ICSOC 2010
  • ICWS 2010


The following projects are (were) under my supervision and/or assistance:

Master Theses

Mark Kloosterhuis, Verification extension for Business Process Modeling (VxBPM) Tool,
University of Groningen, May 2016, supervision by Prof. dr. ir. Marco Aiello.

Piet den Dulk, VxBPMN Designer: A Graphical Tool for Customizable Process Models Using the PVDI Framework,
University of Groningen, September 2014, supervision by Prof. dr. ir. Marco Aiello.

Adam Loorbach, Measuring the efficiency offered to local e-Governments by Service Oriented Architectures,
University of Groningen, August 2010, supervision by Prof. dr. ir. Marco Aiello.

Scientific Internships

Andrés Tello, Business Process Model Checking: using PDVI techniques & the NuSMV model checker tool,
University of Groningen, May 2013, supervision by Prof. dr. ir. Marco Aiello.

Bachelor Theses

Sam van Dijk, Model checking business processes: The search for the most compatible model checker,
University of Groningen, January 2014, supervision by Prof. dr. ir. Marco Aiello.

Robbert-Jan Pijpker, Business Process Variants: a Generation from Templates,
University of Groningen, June 2013, supervision by Prof. dr. ir. Marco Aiello.