Decomposition-based Verification of Global Compliance in Process Choreographies [original]

Decomposition-based Verification of Global

Compliance in Process Choreographies

Walid Fdhila

SBA-Research,

Vienna, Austria

[email protected]g

Stefanie Rinderle-Ma

Faculty of Computer Science

University of Vienna

Vienna, Austria

stefanie.rinderle-ma@univie.ac.at

David Knuplesch

Institute of Databases and Information Systems

Ulm University

Ulm, Germany

da[email protected]

Manfred Reichert

Institute of Databases and Information Systems

Ulm University

Ulm, Germany

[email protected]

Abstract—The verification of global compliance rules (GCR) in

process choreographies (e.g., partner-spanning quality assurance

in supply chains) is crucial and challenging due to the restricted

visibility of the private processes of the collaborating partners.

This paper provides a novel algorithm that decomposes global

compliance rules into assertions that can be verified by the

partners in a distributed way without revealing any private

process details. The decomposition is based on transitivity prop-

erties of the underlying GCR specification. This work uses GCR

based on antecedent and occurrence patterns and illustrates the

transitivity properties based on their specification in first order

predicate logic. It is formally shown that the original GCR can

be reconstructed from the assertions, which ensures the viability

of the approach. The algorithms are prototypically implemented

and applied to several scenarios. The ability of checking global

compliance constitutes a fundamental pillar of any approach

implementing process choreographies with multiple partners.

Index Terms—Distributed and cross-organizational business pro-

cesses, Business rules and compliance management, Business

process compliance, Global compliance rules, Rule decomposition

I. INTRODUCTION

The arrival of technologies such as blockchain and Industry

4.0 has pushed the process-oriented collaboration between

distributed business partners [25], realized by so called process

choreographies. Figure 1 depicts a collaboration diagram of a

supply chain scenario as a composition of the public models

[1] of the partners Manufacturer,Middleman,Special Carrier,

and Supplier. The private models of the partners, in turn,

implement and possibly extend the behavior of the public

models. Private tasks–depicted as dashed boxes in Fig. 1–

are not visible to the partners, whereas public tasks can

realize interaction (message exchange) between two partners.

Although private tasks are usually hidden to other partners,

restrictions over them might exist. In this case, no information

about how and when the task is executed, or how it is con-

nected to the other nodes of the corresponding private model

is visible to the other partners. Usually, this happens when a

collaborating partner imposes the execution of a specific task

which must exist in its private process and comply with a

given rule to another partner. The latter should then assure the

existence of such task, and that it follows the imposed rule.

Assume that the supply chain depicted in Fig. 1 is subject

to a Global Compliance Rule (GCR), which stems from legal

regulations and standards such as GDPR or Sarbanes Oxley.

A GCR constrains actions of multiple partners and/or the

interactions between them. Ensuring the compliance of process

choreographies with a GCR is crucial and challenging [16] as

a partner “only has the visibility of the portion of the process

under its direct control” [26]. In Fig. 1, GCR C1 asks for a

safety check, which is accomplished by a private task at the

Special Carrier. To cope with this issue, assertions can be used.

An assertion (A) is a commitment of a partner guaranteeing

that its private/public process complies with the constraint [8].

In the example, the Middleman agrees to get the permission

of the authority before ordering the sepcial transport (A1).

Special carrier commits to perform a safety check before

transporting the intermediate (A2). Combined, A1 and A2

enable checking GCR C1.

[26] tackles the problem of checking GCR on private tasks

based on IoT-enabled artifacts. The approach presented in this

paper aims to exploit assertions in order to stay independent of

a particular technology such as IoT. The fundamental research

question addressed in this work is as follows:

How to decompose a GCR into derived assertions that can be

checked in a distributed way without violating the privacy of

the involved process partners?

We tackle the question by providing a decomposition algo-

rithm that breaks down the initial GCR into derived assertions.

By combining the derived assertions, in turn, we can re-

construct the original GCR, i.e., the decomposition is lossless.

In turn, the assertions obtained from the decomposition can be

checked by the process partners in a distributed way without

revealing any private details. The decomposition relies on

Manufacturer Middleman

Bulk Buyer .

Special

Carrier

Supplier

Process

order

Order

intermediate

Arrival of

intermediate

Production Final

test

Delivery

of product

Order

Get permission

of authority

FWD order

intermediate

Order

special transport

Safety check

FWD order

intermediate

Order

intermediate

Produce

intermediate

Request

Details

Transport

Details

Prepare

Transport

Order

special transport

Request

Details

Transport

Details

Waybill for

intermediate

Arrival of

intermediate

Waybill for

intermediate

Transport

Intermediate

Transport

intermediate

Get permission

of authority

Safety-Check

Full

quality test

intermediate

Assertion A2 of Middleman

Order specialGet permission

of authority

Assertion A3 of Special carrier

Transport

intermediate

Safety-Check

Public

Task

Special

Carrier

C1: Each transport of the intermediate requires

permission of authority. Further, the transporter

must pass a safety check before.

A1: Middleman assures that he gets permission

of the authority for the special transport

before he orders the special transporter.

A2: Special carrier assures to perform a safety check

before he starts the transport of the intermediate.

Interaction

or Message

Exchange

Assertion

Global compliance rules

Private

Task

Quick test

intermediate

Fig. 1. Running example with four process partners: Supply chain (adapted from [8])

transitivity properties of the underlying GCR specification.

In order to remain independent of a certain language and

technology, we rely on simple rules that consist of antecedent

and occurrence patterns. The transitivity properties are shown

by the example of a translation to first order predicate logic.

Similarly, for example, [29] presents declarative patterns based

on Linear Temporal Logic (LTL). As part of the evaluation,

the correctness of the decomposition algorithm is formally

proven. Moreover, the algorithm is prototypically implemented

and its application is demonstrated along basic choreography

scenarios.

The remainder of the paper is structured as follows: Section

II provides fundamentals. Section III-B deals with the de-

composition algorithm and Sect. IV with the correctness of

the algorithm. Sections V and III-A present details on the

implementation and application of the algorithm. Section VI

discusses related work and Section VII summarizes the paper.

II. FUNDAMENTALS AND TRANSITIVITY THEOREM

This section presents definitions and formal backgrounds for

global compliance rules (GCR) over a process choreography y.

A choreography includes three types of overlapping models:

(i) a private model representing the executable process and

including private activities as well as interactions with other

partners, (ii) a public model (also called the interface of the

process) that solely highlights the interactions of a given

partner, and (iii) a choreography model providing a global

view on the interactions between all partners [7].

The interactions of a single partner are described in a public

model. The public model thus serves as public (restricted)

view on the private model of the partner which “describes

the internal logic of a partner including its private activities and

interactions” [4]. In this paper, we assume that the choreog-

raphy yis sound, i.e., structural and behavioral compatibility

between public models and consistency between public and

private models are given [7]. For a formal definition of process

choreography, we refer the reader to Def. 3 in Appendix A.

We opt for expressing a GCR based on antecedence and

consequence patterns. An antecedence pattern specifies when

a GCR over yshall be triggered. In this situation, the desired

behavior of yis described by related consequence patterns.

Based on execution traces capturing all events related to the

enactment of y, antecedence and consequence patterns are

interpreted as follows: for each match of the antecedence

pattern there must be at least one match of a consequence

pattern. This simple representation of GCR abstracts from a

certain language and technology, i.e., any language can be cho-

sen that supports antecedence and consequence patterns, and

the transitivity properties defined in this paper. Antecedence

and consequence patterns are specified using occurrence and

absence nodes, which either express the occurrence or ab-

sence of events related to the execution of activities or the

exchange of messages in y. We use the following notation:

A: Antecedence occurrence; A: Antecedence absence; A:

Consequence occurrence; A: Consequence absence

In a previous work [6], multiple formal languages employed

for business process compliance modelling and checking (e.g.,

linear temporal logic LTL, event calculus EC, extended com-

pliance rule graph eCRG) were compared. It was proven that

most of these languages can deal with most qualitative time

patterns, and can therefore be used to model the compliance

constructs addressed in this paper. Similar results were proven

in [14]. In order to specify these constructs as well as

transitivity properties required for the GCR decomposition,

this work uses the eCRG formalism [21]. The latter offers

a visual rule notation for expressing compliance rule graphs

over choreographies and is based on first order predicate logic.

Definition 1 specifies those parts of the eCRG formalism that

are necessary for defining GCRs and their decompositions.

In detail, Def. 1 (i) refers to activities and interactions in y,

(ii) allows for exactly one antecedence occurrence pattern per

rule, and (iii) assumes the rules to be structured as trees. As the

decomposition focuses on the interactions between the partners

and their control flows, (i) does not impose any restriction.

Moreover, (iii) contributes to simplify the algorithm. For the

sake of space and simplicity, we restrict the definition of GCR

to one antecedence occurrence pattern (ii), but will extend this

in future work.

Definition 1 (GCR structure): Given a process choreography

y(cf. Def. 3 in Appendix A), let Abe the set of public

and private activities and Ibe the set of interactions in

choreography model G. Then: a GCR ris defined as tree

r= (N, ρ, ϕ, type, pattern, root)with

•Nbeing the set of nodes,

•ρ:N→ {p1...pn}returning the partner responsible for

a node.

•ϕ:N×N→ { 99K,−→} returning the sequence flow

connector of two nodes, i.e., consequence sequence and

antecedence sequence connectors respectively.

•type :N→ A ∪ I mapping each node to an activity or

an interaction, i.e., message exchange.

•pattern :N→ { A,A,C,C}

•root ∈Nbeing the root node with pattern(root) = A

•∀n∈N\ {root}:pattern(n)6=A

•∀n∈Nwith pattern(n) ∈ { A,C}: n is leaf node

We illustrate the translation of a GCR into a First Order

Logic (FOL) expression using basic equivalences as in Def. 2

following below. As shown in the following, equivalences are

also required for ensuring correctness of the decomposition.

Additionally, throughout the paper we consider the conse-

quence sequence connector. This can be easily extended to

antecedence sequence connectors.

Definition 2 (Basic Equivalences): Based on [22] the

following equivalences hold by definition. Predicate x(t, ty)

describes that at the point in time tan activity (message) of

type ty was executed (i.e., sent or received).

•A99K B:⇔ ∀a:x(a, A)→∃b: (x(b, B)∧a<b)

⇔ ∀a∃b:x(a, A)→(x(b, B)∧a<b)

•A99K B:⇔ ∀b:x(b, B)→∃a: (x(a, A)∧a<b)

⇔ ∀b∃a:x(b, B)→(x(a, A)∧a<b)

•A99K B:⇔ ∀a:

x(a, A)→@b: (x(b, B)∧a<b) 

⇔ ∀a, b :x(a, A)→ ¬(x(b, B)∧a < b)

⇔ ∀a, b :x(a, A)→(¬x(b, B)∨b≤a)

•A99K B:⇔ ∀b:

x(b, B)→@a: (x(a, A)∧a < b) 

⇔ ∀b, a :x(b, B)→ ¬(x(a, A)∧ ¬a < b)

⇔ ∀a, b :x(a, A)→(¬x(b, B)∨b≤a)

For example, GCR Production 99K Final test is translated

into: ∀a:x(a, Production)→ ∃b:x(b, Final test)∧a < b.

Relation <expresses a temporal precedence between aand b.

The decomposition algorithm presented in Sect. III-B exploits

the transitivities for GRC as in Theorem 1. Specifically, by

combining transitive relations, where each relation can be

checked locally by a single partner, it becomes possible to

reconstruct the original GCR behavior. Theorem 1 ensures that

the behavior of the derived assertions reproduces the behavior

of the GCR, but not vice versa.

Theorem 1 (Transitivities):

Let A, B, and Cbe three activity or message types. Then:

a. The rightwards transitivity holds:

A99K B∧B99K C⇒A99K C

b. The leftwards transitivity holds:

A99K B∧B99K C⇒A99K C

c. The rightwards zig zag transitivity holds for the conse-

quence absence:

B99K A∧B99K C⇒A99K C

d. The leftwards transitivity holds for the consequence ab-

sence:

A99K B∧C99K B⇒C99K A

In the following, the correctness of Theorem 1 is proven

applying Def. 2.

Proof 1 (Rightwards Transitivity): Let A, B, C be three

activities or interactions. Then A99K B∧B99K C

:⇔ ∀a∃b:x(a, A)→(x(b, B)∧a < b)∧∀b∃c:

x(b, B)→(x(c, C)∧b<c)

⇔ ∀a∃b:x(a, A)→(x(b, B)∧a<b)∧∀b:∃c:

x(b, B)→(x(c, C)∧b < c)

⇒ ∀a∃b, c :x(a, A)→(x(b, B)∧a<b)∧x(b, B)→

(x(c, C)∧b < c)

⇒ ∀a∃b, c :x(a, A)→x(b, B)→(x(c, C)∧a < b <

c)

⇒ ∀a∃c:x(a, A)→(x(c, C)∧a < c)⇒A99K C

q.e.d.

Leftwards transitivity can be proven similarly by replacing ’<’

with ’>’.

Corollary 1: Let A, B, C, and Dbe activities or interactions.

Then

A99K B∧B99K C∧C99K D⇒A99K C∧C99K D

⇒A99K D

Proof 2 (Rightwards Zig Zag Transitivity of Absence): Let

A, B, C be activities or interactions. Then:

B99K A∧B99K C

:⇔ ∀a∃b:x(a, A)→(x(b, B)∧b < a)∧ ∀b, c :

x(b, B)→(¬x(c, C)∨c≤b)

⇔ ∀a∃b:x(a, A)→(x(b, B)∧b < a)∧ ∀b, c :

x(b, B)→(¬x(c, C)∨c≤b)

⇒ ∀a∃b∀c:x(a, A)→(x(b, B)∧b<a)∧x(b, B)→

(x(c, C)→c≤b)

⇒ ∀a∃b∀c:x(a, A)→x(b, B)→(x(c, C)→c≤b <

a)

⇒ ∀a∀c:x(a, A)→(x(c, C)→c≤a)

⇒ ∀a, c :x(a, A)→(¬x(c, C)∨c≤a)⇒A99K C

q.e.d.

Leftwards zig zag transitivity of absence can be proven sim-

ilarly by replacing ’<’ with ’>’ and ’≤’ with ’≥’. The

transitivity of other constructs such as “chaining” or “requires

transitivity” can be found in Appendix B.

III. DECOMPOSING GLOBAL COMPLIANCE RULES

At design time, checking a GCR that solely refers to inter-

actions and/or public activities can be achieved by applying

contemporary compliance checking techniques (cf. [13]) either

on the choreography model or the public models of the

involved partners. By contrast, if a GCR refers to private

activities of different partners, it becomes impossible to check

its correctness as partners cannot view the private process

parts of the other partners and, therefore, cannot identify

the dependencies between the private activities involved in

the GCR. To cope with this, we suggest decomposing the

GCR into a set of assertions of which each can be checked

locally by the corresponding partner. The decomposed rules

then reproduce the behavior of the original GCR.

Decomposition in compliance checking has been exploited

by [32], but only at the process model level in order to

achieve performance gains for the compliance checks. The

paper at hand, first of all, proposes to decompose the global

compliance rule to distribute the compliance checks to the

partners for maintaining the confidentiality of their private

tasks. We start with illustrating the idea and the challenges

of GCR decomposition based on different scenarios. Then the

decomposition algorithm is introduced and explained.

A. GCR Decomposition Scenarios and Discussion

In the following, we use a set of scenarios (cf. Figs. 2 and 3)

to illustrate the GCR decomposition process. For the sake of

readability, in these scenarios we assume a simple compliance

rule involving two tasks of two different partners p1and p2.

In Scenarios 1 – 3, we assume rule A99K B, where the

execution of task Ashall be followed by the one of task B.

For simplicity, we use labels A,B,m1,m2,p1and p2instead

of the actual labels taken from the example of Fig. 1.

•In Scenario 1 there exists a message exchange m1

between p1and p2that fulfills conditions A99K m1and

m199K B. The behavioral and structural compatibility

(cf. Sect. II) between the partner processes ensures that

message m1sent by p1shall be correctly received by p2.

•In Scenario 2 we assume that there is no direct interaction

between p1and p2, but there exists a transitive interaction

through partner p3. Partner p1interacts with p3through

m1and p3interacts with p2through m2. In this sce-

nario, the transitive relations A99K m1,m199K m2,

and m299K Breproduce the behavior of A99K B.

Consequently, partner p3, which is initially not involved

in the GCR becomes involved in the derived assertions.

We call p3an intermediary partner.

•In Scenario 3 we assume that, even though there are

interactions between p1and p2, no direct or transitive

interactions reproduce the behavior of A99K B. As such,

additional message exchanges become necessary to in-

form about the execution state of activities involved in the

GCR. Message exchanges can be either synchronous or

asynchronous. Asynchronous message exchange only al-

lows for reactive GCR checking and, hence, for detecting

violations after their occurrence. Synchronous message

exchange is proactive as it enforces the GCR with new

restrictions to the process models, e.g., the execution of

Bis enabled only after receiving the synchronization

message (i.e. whether Ais or is not executed). Partner

p1shall also inform p2in case Ais not executed, as this

does not prevent Bfrom being executed according to the

GCR.

Rightwards transitivity (cf. Theorem 1.a) directly ensures the

correctness of Scenarios 1 and 3 from Figure 4. It should be

clear that the correctness of Scenario 2 can be directly derived

from Corollary 1 (cf. Sect. II).

For the scenarios depicted in Figure 3, we assume differ-

ent compliance rules, where the antecedent presence B

implies the later consequence absence Ain Scenario 4;

i.e., B99K A, and antecedence presence Brequires the

consequence presence Abefore, in Scenario 5, i.e., A99K B.

•In Scenario 4 (includes an adaptation of the example

of Fig. 1), for partner p1, the execution of Aauto-

matically implies non-execution of m1before and vice

versa (due to the used XOR pattern). Consequently, it

ensures rule m199K A. For partner p2, the execution of

Bis always preceded by the one of m1, which implies

m199K B. The composition of the two rules m199K A

and m199K B, in turn, reproduces the behavior of

B99K A. Similarly to Scenario 2, this dependency can

become more complex and transitive. This example also

Order

special transport

Safety check

Get permission

of authority

Get permission

of authority

Order

special transport

Produce

intermediate

Get permission

of authority

Process Order

Order

intermediate FWD order

intermediate

Order

intermediate

FWD order

intermediate Get permission

of authority

Prepare

Transport

Waybill for

intermediate

Get permission

of authority

Safety Check

Waybill for

intermediate

Middleman - P1 Manufacturer - P1

Special Carrier- P2 Supplier - P2Middleman - P3 Special Carrier - P2Supplier - P1

sync

m1 m1 m2

Scenario (3)

Scenario (1) Scenario (2)

Fig. 2. Scenarios 1–3

Get permission

of authority

Transport

intermediate

Get permission

of authority

Order

special transport

Get permission

of authority

Order

special transport

Get permission

of authority

Quick test

intermediate

Arrival of

intermediate

Arrival of

intermediate

Transport

intermediate

Quick test

intermediate

Scenario (4) Scenario (5)

Special Carrier- P1 Manufacturer - P2 Manufacturer - P2Special Carrier- P1

Fig. 3. Scenarios 4–5

illustrates A99K Band A99K Bin a similar way.

•In Scenario 5, if Bis executed, Ashould have been

executed before. However, the execution of Adoes not

imply that Bis always executed. Regarding p1, the

execution of Aimplies the one of m1and vice versa; i.e.,

A99K m1and A99K m1. Regarding p2, the execution

of Balways implies the one of m1before, but not the

other way around; i.e. m199K B. Since both assertions

refer to the same message exchange m1between p1and

p2, in combination with each other, the two assertions

A99K m1and m199K Bcan reproduce the behavior

of A99K B

The correctness of Scenario 5 concludes from the rightwards

transitivity (cf. Theorem 1.b), whereas Scenario 4 relies on

the zig zag transitivity of the absence (cf. Theorem 1.c).

Figure 4 summarizes the decomposition results of the sketched

scenarios. The latter are used to illustrate selected use cases.

The decomposition process is not limited to these scenarios

and, as aforementioned, the decomposition cannot always be

automated, but might require manual interaction and process-

ing. Altogether, the decomposition eases global compliance

rule checking, where each partner checks its corresponding

derived assertions locally. A GCR is rechecked only if at least

one of the derived assertions is not evaluated to true. Note that

this does not necessarily imply that the GCR is violated.

B. GCR Decomposition Algorithm

This section focuses on the decomposition algorithm and

explains the steps to derive assertions using transitivities.

Algorithm 1 realizes GCR decomposition as set out in Def.

1. It assumes that each node of the GCR is assigned to one

partner being responsible for it. Further on, we assume the

input GCR to be consistent and satisfiable (for dealing with

unsatisfiable and inconsistent rules we refer to [5]). In the

following, we first explain Algorithm 1 step by step and then

illustrate the entire algorithm along Example 1 (see below).

Starting from the Anode (cf. Def. 1), Algorithm 1 walks

outwards through all other nodes of the GCR. Thereby, the

visited parts are copied and become assertions. Wherever

the algorithm walks over a connector between two nodes

nand s, which are assigned to different partners ρ(n)and

ρ(s), the GCR is split at this position as this dependency

cannot be evaluated by a single partner. Next, the algorithm

tries to replicate the connector where the GCR was split

through (transitive) message exchanges between both affected

partners by applying the transitive relationships from Section

II. Therefore, sets n•,•s, and Θare calculated. Depending on

the pattern of s(cf. Def. 1), n•and •scontain the messages

succeeding or preceding nand s. Note that these calculations

have to be accomplished in a decentralized manner by ρ(n)

and ρ(s)themselves as nand smay be private tasks. Next, Θ

combines those messages of n•and •sthat can be combined.

If sis a Cnode (i.e., smust follow n), Θcontains message

tuples (m1, m2)that ensure that nis always followed by

Loading more pages...