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

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

Abstract

A wealth of techniques have been developed over the past decades to help organizations understand their processes, verify correctness against requirements and diagnose potential problems. In general, these techniques for verification 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 each 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, the 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 and the artifacts they apply to. Moreover, we explore the consequences when these terms are used incorrectly. In doing so, we aim to improve transfer from research to practical applications and increase adoption of relevant approaches and new advances in the field by clarifying the relation between available techniques and the intended verification goals.

Keywords: Conformance, Compliance, Verification, Review

BibTeX

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

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

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

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

BibTeX

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

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

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

BibTeX

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

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

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

BibTeX