Heerko

Heerko Groefsema

PhD in Computer Science

Heerko is a researcher at the Distributed Systems group of the University of Groningen, the Netherlands. In addition, Heerko is a (remote) visiting researcher at the Business Processes and Legal Informatics Team, Data61, Commonwealth Scientific and Industrial Research Organisation (CSIRO), Brisbane. 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

Publications

"log data compliance" (, , and ), .

Abstract

This disclosure relates to a computer analysing log data. The computer receives log data comprising traces having log events from respective process executions. The computer creates a stream of log events, wherein the stream is sorted by the event time. The computer iterates over the stream of log events, and for each log event, executes update functions that define updates of a set of variables based on the log events. The set of variables comprises at least one cross-trace variable to calculate an updated value of the set of variables. The update functions define updates of the cross-trace variable in response to the log events of the traces. The computer further executes evaluation functions on the set of variables to determine compliance in relation to the log data based on the updated value. The evaluation functions represent compliance rules based on the set of variables including the cross-trace variable.


BibTeX



urlpdf

Efficient conditional compliance checking of business process models (, and ), In Computers in Industry, ELSEVIER SCIENCE BV, volume 115, .

Abstract

When checking compliance of business processes against a set of business rules or regulations, the ability to handle and verify conditions in both the model and the rules is essential. Existing design-time verification approaches, however, either completely lack support for the verification of conditions or propose costly verification methods that also consider the full data perspective. This paper proposes a novel light-weight verification method, which is preferable over expensive approaches that include the data perspective when considering structural properties of a business process model. This novel approach generates partial models that capture only relevant execution states to the conditions under investigation. The resulting model can be verified using existing model checking techniques. The computation of such partial models fully abstracts conditions from the full models and specifications, thus avoiding the analysis of the full data perspective. The proposed method is complete with respect to the analyzed execution paths, while significantly reducing the state space complexity by pruning unreachable states given the conditions under investigation. This approach offers the ability to check if a process is compliant with rules and regulations on a much more fine-grained level, and it enables a more precise formulation of the conditions that should and should not hold in the processes. The approach is particularly useful in dynamic environments where processes are constantly changing and efficient conditional compliance checking is a necessity. The approach – implemented in Java and publicly available – is evaluated in terms of performance and practicability, and tested over both synthetic datasets and a real-life case from the Australian telecommunications sector.


Keywords: Business process models, Formal verification, Conditional compliance, Data perspective, Temporal logic


BibTeX



urldoi

Variability in business processes: Automatically obtaining a generic specification (, , and ), In Information Systems, PERGAMON-ELSEVIER SCIENCE LTD, volume 80, .

Abstract

The existence of different process variants is inevitable in many modern organizations. However, variability in business process support has proven to be a challenge as it requires a flexible business process specification that supports the required process variants, while at the same time being compliant with policies and regulations. Declarative approaches could support variability, by providing rules constraining process behavior and thereby allowing different variants. However, manual specification of these rules is complicated and error-prone. As such, tools are required to ensure that duplication and overlap of rules is avoided as much as possible, while retaining maintainability. In this paper, we present an approach to represent different process variants in a single compound prime event structure, and provide a method to subsequently derive variability rules from this compound prime event structure. The approach is evaluated by conducting an exploratory evaluation on different sets of real-life business process variants, including a real-life case from the Dutch eGovernment, to demonstrate the effectiveness and applicability of the approach.


Keywords: Business Process Model, Declarative Variability Modeling, Event Structure, Temporal Logic, PROCESS MODELS, CORRECTNESS


BibTeX



urldoi

A Formal Model for Compliance Verification of Service Compositions (, and ), In Ieee transactions on services computing, volume 11, .

Abstract

Business processes design and execution environments increasingly need support from modular services in service compositions to offer the flexibility required by rapidly changing requirements. With each evolution, however, the service composition must continue to adhere to laws and regulations, resulting in a demand for automated compliance checking. Existing approaches, if at all, either offer only verification after the fact or linearize models to such an extent that parallel information is lost. We propose a mapping of service compositions to Kripke structures by using colored Petri nets. The resulting model allows preventative compliance verification using well-known temporal logics and model checking techniques while providing full insight into parallel executing branches and the local next invocation. Furthermore, the mapping causes limited state explosion, and allows for significant further model reduction. The approach is validated on a case study from a telecom company in Australia and evaluated with respect to performance and expressiveness. We demonstrate that the proposed mapping has increased expressiveness while being less vulnerable to state explosion than existing approaches, and show that even large service compositions can be verified preventatively with existing model checking techniques.


Keywords: Service Composition, Business process, Compliance, Verification, Temporal Logic, Colored Petri net, Kripke structure, COMPLIANCE-CHECKING, BUSINESS, SPECIFICATION, SUPPORT


BibTeX



doi

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

BibTeX



Business Process Variability: a study into process management and verification (), Rijksuniversiteit Groningen, .

Abstract

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.


BibTeX



urlpdf

Design-time Compliance of Service Compositions in Dynamic Service Environments (), In 8th IEEEE International Conference on Service Oriented Computing & Applications (SOCA), IEEE (The Institute of Electrical and Electronics Engineers), .

Abstract

In order to improve the flexibility of information systems, an increasing amount of business processes is being automated by implementing tasks as modular services in service compositions. As organizations are required to adhere to laws and regulations, with this increased flexibility there is a demand for automated compliance checking of business processes. Model checking is a technique which exhaustively and automatically verifies system models against specifications of interest, e.g. a finite state machine against a set of logic formulas. When model checking business processes, existing approaches either cause large amounts of overhead, linearize models to such an extent that activity parallelization is lost, offer only checking of runtime execution traces, or introduce new and unknown logics. In order to fully benefit from existing model checking techniques, we propose a mapping from workflow patterns to a class of labeled transition systems known as Kripke structures. With this mapping, we provide pre-runtime compliance checking using well-known branching time temporal logics. The approach is validated on a complex abstract process which includes a deferred choice, parallel branching, and a loop. The process is modeled using the Business Process Model and Notation (BPMN) standard, converted into a colored Petri net using the workflow patterns, and subsequently translated into a Kripke structure, which is then used for verification.


Keywords: Business Process Management, BPMN, Petri net, Kripke models, Verification, Temporal Logic


BibTeX



pdf

A survey of formal business process verification: From soundness to variability ( and ), In Proceedings of International Symposium on Business Modeling and Software Design, SciTePress, .

Abstract

Formal verification of business process models is of interest to a number of application areas, including checking for basic process correctness, business compliance, and process variability. A large amount of work on these topics exist, while a comprehensive overview of the field and its directions is lacking. We provide an overview and critical reflections on existing approaches.


Keywords: Business Process Management, Verification, Model Checking, Survey


BibTeX



pdf

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

BibTeX



url

Business Process Variability: A Tool for Declarative Template Design (, and ), In Service-Oriented Computing, Springer, volume 7221, .

Abstract

To lower both implementation time and cost, many Business Process Management tools use process templates to implement highly recurring processes. However, in order for such templates to be used, a process has to adhere substantially to the template. Therefore, current practice for processes which deviate more than marginally is to either manually implement them at high costs, or for the business to inflexibly comply to the template. In this paper, we describe a tool which demonstrates a variability based solution to process template definition.


BibTeX



doi

Declarative Enhancement Framework for Business Processes (, and ), In Service-Oriented Computing (G Kappel, Z Maamar, HR MotahariNezhad, eds.), Springer, volume 7084, .

Abstract

While Business Process Management (BPM) was designed to support rigid production processes, nowadays it is also at the core of more flexible business applications and has established itself firmly in the service world. Such a shift calls for new techniques. In this paper, we introduce a variability framework for BPM which utilizes temporal logic formalisms to represent the essence of a process, leaving other choices open for later customization or adaption. The goal is to solve two major issues of BPM: enhancing reusability and flexibility. Furthermore, by enriching the process modelling environment with graphical elements, the complications of temporal logic are hidden from the user.


Keywords: BPM, Variability, Temporal Logic, e-Government


BibTeX



pdfdoi

Requirements and Tools for Variability Management (, and ), In Computer Software and Applications Conference Workshops (COMPSACW), IEEE (The Institute of Electrical and Electronics Engineers), .

Abstract

Explicit and software-supported Business Process Management has become the core infrastructure of any medium and large organization that has a need to be efficient and effective. The number of processes of a single organization can be very high, furthermore, they might be very similar, be in need of momentary change, or evolve frequently. If the ad-hoc adaptation and customization of processes is currently the dominant way, it clearly is not the best. In fact, providing tools for supporting the explicit management of variation in processes (due to customization or evolution needs) has a profound impact on the overall life-cycle of processes in organizations. Additionally, with the increasing adoption of Service-Oriented Architectures, the infrastructure to support automatic reconfiguration and adaptation of business process is solid. In this paper, after defining variability in business process management, we consider the requirements for explicit variation handling for (service based) business process systems. eGovernment serves as an illustrative example of reuse. In this case study, all local municipalities need to implement the same general legal process while adapting it to the local business practices and IT infrastructure needs. Finally, an evaluation of existing tools for explicit variability management is provided with respect to the requirements identified.


Keywords: workflow management software, software architecture, business data processing, web services


BibTeX



pdfdoi

A survey of variability management requirements (, and ), In 5th SIKS/BENAIS Conference on Enterprise Information Systems, EIS 2010, CEUR Workshop Proceedings (CEUR-WS.org), volume 662, .

BibTeX



Thesis

Thesis

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.

Teaching

Courses

The following courses are (were) taught with my assistance:

  • Advanced Object-Oriented Programming (2020-2021)
  • Scalable computing (2020)

Students

The following student 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

Merlijn Frikken, Conversion of Business Process Modeling Notations,
University of Groningen, December 2020.

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.

Tools & Packages

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.

BPM Petri Net Package

The BPMPetriNet package provides a Petri net implementation for Business Process Modeling. The package provides the following functionality:

  • Several place/transition net implementations (place/transition net and a data-driven net)
  • (Un)Marshalling place/transition nets (from) to pnml format.
  • Unfolding place/transition nets into an event structure.
  • Conditional evaluation of guards using expressions.

VxBPM

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.

ProVariant

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.

MicroPython HID library

This personal project offers implementations of Human Interface Devices (HID) over Bluetooth Low Energy (BLE) GATT for MicroPython. The library has been tested using an ESP32 development board (TinyPICO) as the peripheral and Windows 10 as the central. Examples and basic implementations of HID devices are available for

  • Keyboard,
  • Mouse, and
  • Joystick.

This library is NOT intended to offer functionality for every possible HID device configuration. Instead, the library is designed to offer basic well-documented classes that you can extend to fit your HID device needs. For example, the Mouse class offers a three button mouse with vertical scroll wheel. If you plan on developing a gaming mouse with eight buttons and both vertical and horizontal wheels, you will need to extend the Mouse class and overwrite the required functions to include a new HID report descriptor.

Reviews

Journal Review Invitations:

  • Transactions on Services Computing (2017, 2022)
  • Journal of Software and Systems Modeling (2018, 2021)
  • Automated Software Engineering (2019)
  • Computers in Industry (2016, 2017)
  • International Journal on Software Tools for Technology Transfer (2012)

Programme Committee Memberships:

  • Applications of Intelligent Systems (APPIS 2020),
    January 7 - 12, 2020, Las Palmas de Gran Canaria, Spain.
  • Applications of Intelligent Systems (APPIS 2019),
    January 7 - 12, 2019, Las Palmas de Gran Canaria, Spain.
  • 7th European Conference on Service-Oriented and Cloud Computing (ESOCC 2018),
    September 12 - 14, 2018, Como, Italy.
  • Applications of Intelligent Systems (APPIS 2018),
    January 8 - 12, 2018, Las Palmas de Gran Canaria, Spain.
  • 6th European Conference on Service-Oriented and Cloud Computing (ESOCC 2017),
    September 27 - 29, 2017, Oslo, Norway.
  • 5th European Conference on Service-Oriented and Cloud Computing (ESOCC 2016),
    September 5 - 7, 2016, Vienna, Austria.

Review Invitations:

  • 32nd International Conference on Advanced Information Systems Engineering (CAISE 2020),
    June 8 - 12, 2020, Grenoble, France.
  • 2019 IEEE International Conference on Big Data (IEEE BigData 2019),
    December 9 - 12, 2019, Los Angeles, CA, USA.
  • 11th IEEE International Conference on Service Oriented Computing and Applications (SOCA 2018),
    November 6 - 9, 2018, Paris, France.
  • 16th International Conference on Business Process Management (BPM 2018),
    September 9 - 14, 2018, Sydney, Australia.
  • 24th International Conference on Web Services (ICWS 2017),
    June 25 - 30, 2017, Honolulu, Hawaii, USA.
  • 16th International Conference on Web Information Systems Engineering (WISE 2015),
    November 1 - 3, 2015, Miami, Florida, USA.
  • 8th IEEE International Conference on Service Oriented Computing & Applications (SOCA 2015),
    October 19 - 21, 2015, Rome, Italy.
  • 18th International Conference on Principles of Distributed Systems (OPODIS 2014),
    December 16 - 19, 2014, Cortina d'Ampezzo, Italy.
  • 7th IEEE International Conference on Cloud Computing (Cloud 2014),
    June 27 - July 2, 2014, Anchorage, Alaska, USA.
  • 21st International Conference on Cooperative Information Systems (CoopIS 2013),
    September 11 - 13, 2013, Graz, Austria.
  • 20th International Conference on Web Services (ICWS 2013),
    June 27 - July 2, 2013, Santa Clara Marriott, California, USA.
  • 5th IEEE International Conference on Cloud Computing (Cloud 2012),
    June 24 - 29, 2012, Honolulu, Hawaii, USA.
  • 4th IEEE International Conference on Cloud Computing (Cloud 2011),
    July 4 - 9, 2011, Washington DC, USA.
  • 9th IEEE International Conference on Web Services (ICWS 2011),
    July 4 - 9, 2011, Washington DC, USA.
  • 18th International Conference on Cooperative Information Systems (CoopIS 2010),
    October 27 - 29, 2010, Crete, Greece.
  • 8th International Conference on Service Oriented Computing (ICSOC 2010),
    December 7 - 10, 2010, San Francisco, California, USA.
  • 9th IEEE International Conference on Web Services (ICWS 2010),
    July 5 - 10, 2010, Miami, Florida, USA.