Distributed Systems

Dr. Heerko Groefsema

Researcher

  • 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. 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
  2. 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
  3. 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


    urlpdfdoi
  4. 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


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

    Abstract

    This paper presents the integration of two plugins, a declarative process specification generator and a compliance verifier, into the Apromore advanced business process analytics platform. The integrated toolchain has a range of applications of interest to both practitioners and researchers. For example, it can be used in the areas of business process compliance, flexibility and variability. The generator can extract a set of formal specifications that declaratively describe a set of business process variants; whereas the verifier can check whether temporal properties over business process models hold. The verifier can use two different model checker tools: NuSMV2 and NuXMV. These plugins allow business analysts to verify if a newly developed process model adheres to rules and regulations or a specification dictated by existing process model variants.

    BibTeX


    urlpdf

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