Distributed Systems

Heerko Groefsema

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


    urldoi
  2. 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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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


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


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


    urlpdfdoi
  12. Imperative versus declarative process variability: Why Choose? (, and ), .

    Abstract

    Variability is a powerful abstraction in software engineering that allows managing product lines and business processes requiring great deals of change, customization and adaptation. In the field of Business Process Management (BPM) the increasing deployment of workflow engines having to handle an increasing number of instances has prompted for the strong need for variability techniques. The idea is that parts of a business process remain either open to change, or notfully dened, in order to support several versions of the same process depending on the intended use or execution context. The goal is to support two major challenges for BPM: re-usability and flexibility. Existing approaches are broadly categorized as Imperative or Declarative. We propose Process Variability through Declarative and Imperative techniques (PVDI), a variability framework which utilizes temporal logic to represent the basic structure of a process, leaving other choices open for later customization and adaptation. We show how both approaches to variability excel for different aspects of the modeling and we highlight PVDI's ability to take the best of both worlds. Furthermore, by enriching the process modeling environment with graphical elements, the complications of temporal logic are hidden from the user. To show the practical viability of PVDI, we present tooling supporting the full PVDI lifecycle and test its feasibility in theform of a performance evaluation.

    BibTeX


    urlpdf
  13. Declarative Enhancement Framework for Business Processes (, and ), In Service-Oriented Computing (G. Kappel, Z. Maamar, H.R. Motahari Nezhad, 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


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


    urlpdf
  15. 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


    urlpdfdoi