Formal Development of Choreographic Business Processes
LIMOS, Clermont-Ferrand, 8 juin 2017

Pascal Poizat
Université Paris Nanterre
Sorbonne Universités, UPMC Univ Paris 06, UMR 7606, LIP6
CNRS, UMR 7606, LIP6

joint work with M. Güdemann, H. N. Nguyen, G. Salaün, L. Ye, and F. Zaïdi

A Short Comment on (Formal) Models

In this talk, formal models are Transition Systems (LTS, STG)
in these models, ! stands for emission and ? stands for reception

why? mainly because they have a good tool support
e.g., model-checkers and equivalence-checkers in CADP
but also because they support numerous model transformations
e.g., from Business Process languages and notations (WS-BPEL, BPMN)

>Diving into Choreographies

The Shop-n-Deliver Collaboration

three participants : buyer, vendor, and shipper

A request for goods first takes place.

If the goods are available, a shipping request
and then a delivery are achieved.

Else, a cancellation notification is sent (vendor to buyer).

Local Views over Shop-n-Deliver

orchestration models

centered on a specific role
buyer or vendor or shipper

the view is local to the role of interest

captures conversations
between the role and its partners

e.g., WS-BPEL code

Global View over Shop-n-Deliver

choreography interconnection model

takes into account all roles
buyer and vendor and shipper

the view is global
with internal details of the roles

captures conversations
between all roles
interaction is not central

e.g., BPMN collaboration diagram

Global View over Shop-n-Deliver

choreography interaction model

takes into account all roles
buyer and vendor and shipper

the view is global
without internal details of the roles

captures conversations
between all roles
interaction is central

e.g., BPMN choreography diagram
since BPMN 2.0

Conclusion on Global vs. Local Views

global view: interactions matter, good for specification

A request for goods first takes place (buyer to vendor).
If the goods are available, a shipping request (vendor to shipper) and then a delivery (shipper to buyer) are achieved. Else, a cancellation notification is sent (vendor to buyer).

local view: peers matter, good for implementation

The buyer issues requests about goods and is notified about cancellation or gets the goods.
The vendor checks if the goods are available and sends cancellation notification or requests shipping. The shipper ships goods upon request.

Top-Down Development

A form of generative development
1. interaction skeletons are generated using projection from the choreography
2. conformance of the skeletons (composition) to the choreography is verified
3. interaction skeletons are implemented

Bottom-Up Development

A form of development guided by reuse
1. local contracts are extracted from reused (design time) or dynamically bound (runtime) peers
2. conformance of the contracts (composition) to the choreography is verified

>VerChor

[Güdemann et al, IEEE Trans. Services Computing, 9(4), 2016]

VerChor framework

Synchronizability ()

objective: avoid state-space explosion due to asynchronous communication

synchronizable?(P1, ..., Pn) ⇔ synch(P1, ..., Pn) ≡ asynch(P1, ..., Pn)
where synch is the synchronous product and asynch is the asynchronous product (buffers)
takes into account the emission time in the asynchronous product
synchronizable?(P1, ..., Pn) ⇔ synch(P1, ..., Pn) ≡ asynch-1(P1, ..., Pn)
[Basu et al, POPL'12], where asynch-1 is the 1-bounded asynchronous product
synchronizable?(C) ⇔ synchronizable?(C↓1, ..., C↓n)

Realizability () & Conformance ()

objective: check if peers can be implemented by (natural) projection or be reused

realizable?(C) ⇔ C ≡ Π(C↓1, ..., C↓n)
where Π is an operation that yields the semantics of the peers collaboration
realizable?(C) ⇔ synchronizable?(C↓1, ..., C↓n) ∧ C ≡ synch(C↓1, ..., C↓n)
[Basu et al, POPL'12]
conform?(C, P1, ..., Pn) ⇔ synchronizable?(P1, ..., Pn) ∧ C ≡ synch(P1, ..., Pn)

Choreography Development in VerChor

From Formal Framework to Formal IDE

Online Shopping 1.0: BPMN

Choreography Intermediate Format (CIF)

pivot model for choreography-related model transformation
front-end: BPMN
back-end: LNT
currently being evolved into PIF

workflow constructs
inspired but simplified wrt. BPMN
state-machine encoding

BPMN → CIF model transformation
plain old Java over EMF meta-models
part of the Formal Model Transformations framework

Online Shopping 1.0: CIF

CIF → LNT

state machine encoding
LNT (LOTOS NT) process algebra
use of patterns for CIF constructs
complex for inclusive gateways

Verification Scripts (SVL)

SVL scripts are generated to compute models (LTS)
choreography model
peer models if needed (projection using hiding + reduction)
buffer models
composition models (synch and asynch-1)

SVL scripts are generated to check for properties
synchronizability
realizability

using these "Makefile" formal verification scripts, all tasks are automated
including counter-example extraction in case some property does not yield

Online Shopping 1.0: LNT and SVL

Online Shopping 2.0: BPMN

>SChorA

[Nguyen et al, ICSOC'12] [Nguyen et al, ISSRE'13]

SchorA tool

The ChorD Language

Based on [Qiu et al, WWW'07], extended with support for data

L	semantics
1	skip
α	interaction
L1; L2	sequence
L1 + L2	choice
L1 \| L2	parallelism
L1 [> L2	interruption
[φ] ▹ L	if-then
[φ] * L	while

α	choreography language semantics
o[a,b].x	interaction o from a to b ← no data?

α	choreography language semantics
o[a,b].x	interaction o from a to b ← binds x?

α	choreography language semantics
o[a,b].x	interaction o from a to b, x is not bound
o[a,b].<x>	interaction o from a to b, x is bound

no need for τs since we have choice.

shopping = request[buyer,vendor].<x>;
[x≤0] * (error[vendor,buyer]; request[buyer,vendor].<x>);
confirm[vendor,buyer].x

The ChorD Language

Based on [Qiu et al, WWW'07], extended with support for data

L	semantics
1	skip
α	interaction
L1; L2	sequence
L1 + L2	choice
L1 \| L2	parallelism
L1 [> L2	interruption
[φ] ▹ L	if-then
[φ] * L	while

α	role language semantics
o[a,b]?x	reception o in a from b, x is not bound
o[a,b]?<x>	reception of o in a from b, x is bound
o[a,b]!x	emission of o in a to b, x is not bound
o[a,b]!<x>	emission of o in a to b, x is bound
τ	internal action

vendor = request[buyer,vendor]?<x>;
[x≤0] * (error[vendor,buyer]!; request[buyer,vendor]?<x>);
confirm[vendor,buyer]!x

Symbolic Transition Graphs (STG)

Labelled Transition Systems extended with support for data
[Hennessy and Lin, TCS:138(2), 1995], renamings/extensions (STGA, STS, IOLTS, ...) by others
used for symbolic verification, e.g., WS-BPEL testing in [Bentakouk et al, TESTCOM'07]

13 transformation rules from ChorD to STG

request[buyer,vendor].<x>;
[x≤0] * (error[vendor,buyer]; request[buyer,vendor].<x>);
confirm[vendor,buyer].x

Choreography Development in SChorA

Conformance and Data

Conformance is a relation between a specification and an implementation

approach	data	\| support using	loops	assignments	equivalence
[Busi et al, Coordination'06]	yes	closure	no	yes	branching bisimulation
[Li et al, TASE'07]		closure	yes	yes	weak bisimulation
[Kazhamiakin et Pistore, WS-FM'06]		bound domains	yes	no	branching bisimulation

closure does not work for open choreographies, e.g., o1[a,b].<x>; [x>0] ▹ o2[b,a].x
bound domains still yield state space explosion if LTS are used
possibility to have internal actions in peers, hence in implementations
symbolic branching bisimulation
conformance is not always just true or false
if x ≥ 0, Impl = ([x≥0] ▹ confirm[a,b].x + [x<0] ▹ cancel[a,b].x) is conform to Spec = confirm[a,b].x
most general constraint for conformance

Conformance Verification

hide (τ) additional interactions in the implementation
these interactions may have been added by the developper to reach conformance
they may also result from peers interacting with partners outside the scope of the choreography
compute the most general constraint ρ over data exchanged between peers to achieve conformance
modification of [Li and Chen, TACAS'99], symbolic weak bisimulation → symbolic branching bisimulation
ρ is obtained as a Predicate Equation System (PES)
verify ρ using the Z3 SMT solver
transformation from PES to the Z3 input language
reach verdict (true / false / maybe / inconclusive)
if [ρ=false]↝ unsat then ρ is always true and we have conformance
else verdict based on [ρ=true]: unsat → false, sat → maybe, and timeout → inconclusive

Choreography Development in SChorA

Realizability and Data

A choreography is realizable if we can generate conform peers using projection

approach	synchr. communication	asynchr. communication	#causality semantics
[Sun et al, APSEC'10]	yes	no	1

4 different causality semantics for m[a,b]; n[c,d]
[Lanese et al, SEFM'08] synch, send-asynch, receive-asynch, disjoint-asynch
o1[b,a]; o2[c,a]: for synch, for send-asynch (b.o1! ≺ c.o2! not ensured)
o1[a,b]; o2[a,c]: for synch, for receive-asynch (b:o1? ≺ c.o2? not ensured)
o1[a,b]; o2[c,a]: for synch, for disjoint-asynch (b:o1? ≺ c.o2! not ensured)
full-support for data
o1[c,a]<x>; [x>0] ▹ o2[a,b]; [x≤0] ▹ o3[c,d] is realizable (dead parts)
o1[a,c].<x>; ([x>0] ▹ o2[a,b] + [x<0] ▹ o3[c,d]) is realizable (choice based on known data)
realizability achieved using a smart projection
intrusive control well-suited for

Smart Projection

prune unreachable transitions and states
these are parts of the choreography that are not consistent
connect consecutive interactions with different sender/receiver
[Lanese et al, SEFM'08] e.g., o1[a,b].<x>; o2[c,d].<y> → o1[a,b].<x>; X[a,c]; o2[c,d].<y> (send-asynch)
synchronize choice branches
[Qiu et al, WWW'07] role-based, o1[a,b] + o2[a,c] + o3[d,e] → o1[a,b] + o2[a,c] + X[a,d]; o3[d,e] (send-asynch) nothing to do if data-based, o1[a,c].<x>; ([x>0] |> o2[a,b] + [x<0] |> o3[c,d])
exchange information relative to data constraints between peers
o1[a,b].<x>; o2[c,d].x → o1[a,b].<x>; X[b,c].x; o2[c,d].x (disjoint-asynch)

Example

Conclusion

choreographies are central in distributed system development
well-suited for global specifications with interaction as a 1st class citizen
support reasoning and rapid development through generative approaches

formal methods integrate well in choreography-based development
formal grounding - synchronizability, realizability, conformance, control
tool development - VerChor and SChorA (both open source)

going further?
you like theoretical issues → classes of choreographies or parameterized BP
you like practical issues → BP evolution or BP product lines
you want to play collective → join us on PIF and BP verification API

Formal Development of Choreographic Business Processes LIMOS, Clermont-Ferrand, 8 juin 2017

A Short Comment on (Formal) Models

>Diving into Choreographies

The Shop-n-Deliver Collaboration

Local Views over Shop-n-Deliver

Global View over Shop-n-Deliver

Global View over Shop-n-Deliver

Conclusion on Global vs. Local Views

Top-Down Development

Bottom-Up Development

>VerChor

Synchronizability ()

Realizability () & Conformance ()

Choreography Development in VerChor

From Formal Framework to Formal IDE

Online Shopping 1.0: BPMN

Choreography Intermediate Format (CIF)

Online Shopping 1.0: CIF

CIF → LNT

Verification Scripts (SVL)

Online Shopping 1.0: LNT and SVL

Online Shopping 2.0: BPMN

>SChorA

The ChorD Language

The ChorD Language

Symbolic Transition Graphs (STG)

Choreography Development in SChorA

Conformance and Data

Conformance Verification

Choreography Development in SChorA

Realizability and Data

Smart Projection

Example

Example

Example

Conclusion

Formal Development of Choreographic Business Processes
LIMOS, Clermont-Ferrand, 8 juin 2017