Distributed Systems

Dr. Heerko Groefsema

Assistant Professor

  • Room number: 591
  • E-mail: h.groefsema [at] rug.nl
  • Personal website: Heerko Groefsema

Research

  • Service Oriented Architecture
  • Business Process Management
  • Variability Management

PhD Thesis

  1. 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

Recent publications

  1. Managing and Anticipating Out-of-Order Events in Online Compliance Monitoring (, , and ), In 37th International Conference on Advanced Information Systems Engineering, CAiSE 2025, Springer, .

    Abstract

    When monitoring compliance of event streams at runtime, it is usually assumed that the events are received in the order in which they are produced. However, in reality, event data is typically transmitted from distributed sources and may be received out-of-order as a result. This is problematic for the compliance analysis in terms of accuracy, latency and computational efficiency. In this paper, we present an approach to manage these problems by exploiting knowledge of the event sources to identify the reliable prefix of the event stream that is guaranteed to be in order, allowing a reliable analysis on that prefix. Subsequently, we use the prefix alignment of the observed event stream and a process model to quantify its reliability and identify events that might arrive out-of-order, allowing to calculate a confidence score of compliance results. This improves efficiency and provides compliance results with awareness of potential uncertainty, enabling decision makers to respond appropriately to the identified issues.


    Keywords: Out-of-Order Event Streams, Process Models, Online Monitoring, Compliance, Conformance, Alignments

    BibTeX
  2. Supporting business process variability through declarative process families ( and ), In Computers in Industry, volume 159-160, .

    Abstract

    Organizations use business process management systems to automate processes that they use to perform tasks or interact with customers. However, several variants of the same business process may exist due to, e.g., mergers, customer-tailored services, diverse market segments, or distinct legislation across borders. As a result, reliable support for process variability has been identified as a necessity. In this article, we introduce the concept of declarative process families to support process variability and present a procedure to formally verify whether a business process model is part of a specified process family. The procedure allows to identify potential parts in the process that violate the process family. By introducing the concept of process families, we allow organizations to deviate from their prescribed processes using normal process model notation and automatically verify if such a deviation is allowed. To demonstrate the applicability of the approach, a simple example process is used that describes several variants of a car rental process which is required to adhere to several process families. Moreover, to support the proposed procedure, we present a tool that allows business processes, specified as Petri nets, to be verified against their declarative process families using the NuSMV2 model checker.


    Keywords: Business processes, Variability, Declarative, Process families, Temporal logic, Verification

    BibTeX


    doi
  3. Cross-Instance Regulatory Compliance Checking of Business Process Event Logs (, , , , and ), In IEEE Transactions on Software Engineering, volume , .

    Abstract

    Event logs capture the execution of business processes, such that each task is represented by an event and each individual execution is a chronological sequence of events, called an event trace. Event logs allow after-the-act and runtime analysis of deployed business processes to verify whether their execution complies with regulations and business requirements. Checking the compliance of a single sequence of events in a trace is straightforward and a number of approaches have been proposed to address this. However, some regulations or business rules span multiple process instances and a cross-instance analysis is required. In order to check whether such requirements are maintained at all times, multiple traces need to be analysed together, which can result in a combinatorial computational complexity. In this paper, we present a novel approach that efficiently checks runtime regulatory compliance based on event logs, while supporting cross-instance rule evaluation and extensible function evaluation over sequences of attribute data values. The efficiency and applicability of the proposed method is tested in a two-pronged evaluation, showing a significant improvement over existing techniques with respect to capabilities as well as computational complexity. The approach presented in this paper is subject to a patent application, with patent number WO2021/248201.


    Keywords: Business process, Event log, Compliance, Regulations, Cross-instance, Instance-spanning, Runtime verification

    BibTeX


    doi
  4. On the Use of the Conformance and Compliance Keywords During Verification of Business Processes (, and ), In Business Process Management Forum (C. Di Ciccio, R. Dijkman, A. del Río Ortega, S. Rinderle-Ma, eds.), Springer, .

    Abstract

    A wealth of techniques have been developed to help organizations understand their processes, verify correctness against requirements and diagnose potential problems. In general, these verification techniques allow us to check whether a business process conforms or complies with some specification, and each of them is specifically designed to solve a particular business problem at a stage of the BPM lifecycle. However, the terms conformance and compliance are often used as synonyms and their distinct differences in verification goals is blurring. As a result, the terminology used to describe the techniques or the corresponding verification activity does not always match with the precise meaning of the terms as they are defined in the area of verification. Consequently, confusion of these terms may hamper the application of the different techniques and the correct positioning of research. In this position paper, we aim to provide comprehensive definitions and a unified terminology throughout the BPM lifecycle. Moreover, we explore the consequences when these terms are used incorrectly. In doing so, we aim to improve adoption from research to practical applications by clarifying the relation between techniques and the intended verification goals.

    BibTeX


    urldoi
  5. 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


    urlpdfdoi

(For more publications go to Heerko's publication page)