=Paper=
{{Paper
|id=Vol-494/paper-2
|storemode=property
|title=Verifying A-Priori the Composition of Declarative Specified Services
|pdfUrl=https://ceur-ws.org/Vol-494/mallowawesomepaper2.pdf
|volume=Vol-494
|dblpUrl=https://dblp.org/rec/conf/mallow/ChesaniMMT09
}}
==Verifying A-Priori the Composition of Declarative Specified Services==
https://ceur-ws.org/Vol-494/mallowawesomepaper2.pdf
1
Verifying A-Priori the Composition of Declarative
Specified Services.
Federico Chesani, Paola Mello, Marco Montali, Paolo Torroni
Abstract—Service Oriented Architectures are knowing a wide the task of ensuring that two services can successfully coop-
success, thanks to the maturity of standards and implementa- erate is demanded to the software architect that is designing
tions. Moreover, the possibility of composing complex systems the system. Analogously, ensuring that the composed system
starting from simpler services is becoming supported by in-
dustrial tools, although still immature at the standard level. will exhibit certain properties is a task that directly burden the
However, the a-priori verification aspect, i.e. the capability of developer. Although such guarantees can be verified by human
determining before executing the system if it exhibits some users with small systems, there are serious doubts of achieving
particular behaviour, is still matter of an intense research effort. such results when the composed systems grow in dimension
In this paper we investigate the a-priori verification of bottom- and interaction complexity. Hence, the task of automatically
up build systems from the behavioural viewpoint, where a
choreography is not known at the beginning of the developing verifying a service composition a-priori (during the designing
process, but rather it is verified only later. We focus on the phase), is of the fundamental importance to foster the service
problem of deciding if, given a set of services, there can be composition and the “off-the-shelf” composition model .
some fruitful interaction among them; if yes, we focus also Several approaches have been adopted to address the verifi-
on the problem of determining such interaction. Our approach cation of service composition. A very common way consist
is based on specifying the services by means of the ConDec
declarative language, and by exploiting its translation to the of checking one service against a global description of a
SCIFF Framework to automatically perform the verification task. system, like in [1], [8]. In order to succeed, the following
assumptions are usually made: 1) there is a description of
Index Terms—ConDec Service Modeling, Declarative Lan- the whole system, from a global point of view; 2) there is
guages, A-priori Verification, Logic Programming. a description of the service under testing, such description
not necessarily matching with the service internals; and 3) all
services except the one under testing will behave as prescribed
I. I NTRODUCTION
by the global specification (hence the global description can be
ERVICE ORIENTED COMPUTING emerged recently as
S an architectural paradigm for modeling and implement-
ing business collaboration within and across organizational
used to reason upon the other services behaviour). Given this
setting, the verification task determines if the behaviour of the
service under testing is compatible with the global description
boundaries. The Web Service technology, currently the most (also named choreography). The choreography is intended as
advanced implementation of Service Oriented Architecture a sort of “legal, tight contract”, and plays a double role: it
(SOA) principles, is almost established as the standard tech- specifies the “boundaries” for the service under testing, and
nology for current business implementations, thanks to the provides the expected behaviour of the other (unknown) peers.
support it has received from the academics as well as from The obvious advantage of such approach is that the verification
the industrial partners. task involves only a service description and a choreography:
A key aspect in the success of Service Oriented Computing the component “certified” as compliant can be then adopted
(SOC) is the possibility of composing different, heteroge- to play a certain role within the global system, independently
neous services, yet achieving a complex system starting from of the other peers.
more simple components. Interoperability at the level of data In this paper we investigate the verification of service com-
exchange, as well as at the level of service location and position from another viewpoint. We start from the assumption
invocation, has been guaranteed by standards like WSDL [6]. that, at least in the beginning steps, a global choreography
Industrial tools are becoming available to support also the is not defined (or is not yet available). Beside a “top-down”
composition process, too. Although languages for defining developing method, where the developer starts designing the
composition rules and models have been proposed, but none choreography and proceeds to refine the components in several
of them has enjoyed the maturity level of the other standards. steps, there is also a common “bottom-up” projecting style,
Initial proposals like BPMN [15], WS-CDL [7] and BPEL [3] where the developer simply starts to build up her application
have been criticized for their intrinsic procedural nature, while by putting together the already available components. If this
the need for open, declarative approaches has been recognized is the case, the models of all parties (called local models
only later [4], [14]. thereafter) are directly composed, in order to make them
Automatic verification of properties regarding the be- interact and mutually benefit from each other, as in Figure
havioural aspects of the composed systems is deemed as a cru- 1a.
cial step, but a comprehensive solution is lacking. Currently, The first problem we try to address is: given a composition
DEIS - Department of Electronics, Informatics and Systems, University of of services, does exist a successful interaction? If yes, how
Bologna. name.surname@unibo.it is made such interaction? In case of a positive answer to the
2
(a) Bottom-Up (b) Top-Down
Fig. 1. Developing complex systems using simpler services.
first question, we say that the models are compatible. Beside Section III and in Section IV we try to better capture the notion
the yes/no answer, we deem as fundamental also knowing of compatible services (compatible models of services) and of
as much as possible about such interactions. E.g., knowing compliance to a choreography. In Section V we show how such
in advance the supported interaction traces would help in properties are automatically verified exploiting the ConDec
the analysis of the global system features and properties. Language and its translation into the SCIFF Framework [2].
Of course, “compatible” does not mean that a successful Finally we conclude and discuss future works.
interaction will be effectively achieved at run-time.
A second problem we discuss in this work is about chore- II. M ODELING A S ERVICE BY M EANS OF THE C ON D EC
ographies, intended no more as a tight contract to be respected, L ANGUAGE
but rather as a set of constraints representing the desired ConDec is a declarative, graphical language proposed by
properties of the system. In this view, choreographies are not van der Aalst and Pesic [13] within the research field of
intended as the set of requirements each service should fulfill Business Process Management (BPM). It aims to support
to interact, but rather a set of desired features that the global specification, enactment and monitoring of Business Process,
system will exhibit. Roughly, this problem can be formulated by means of constraints among activity executions. Constraints
as follow: given a compatible set of services, does exists are declaratively expressed, as the authors claim that the
some successful interaction that honors the choreography adoption of a declarative approach fits better with complex, un-
constraints? If yes, how is made such interaction? Also in predictable processes, where a good balance between support
this case we aim to know not only a yes/no answer, but also and flexibility must be found. Although it has been originally
some sort of fully/partially specified interaction trace. proposed in the BPM context, it has been applied also in
In our approach, services and choreographies are repre- the far broader field of SOA. Former applications of ConDec
sented by means of a declarative language, and in particular regarded choreographies specification; in this paper, we adopt
using the ConDec language [13]. We agree with the critics it to represent also service local models.
moved to procedural approaches in [4], [14]. In particular,
choreographies (intended as a set of properties or constraints A. The ConDec Language
of the final resulting system) are more naturally represented in A ConDec model mainly consists of two parts: a set of
terms of declarative rules/constraints, rather than by sentences activities, representing atomic units of work, and a set of rela-
of a procedural language. In this work, we extend the original tionships which constrain the way activities can be executed,
ConDec model to the concepts of roles, and provide definition and are therefore referred to as constraints. Constraints can be
of service composition compatibility on the resulting ConDec interpreted as policies/business rules, and may reflect different
models. kinds of knowledge: external regulations and norms, internal
The ConDec semantics originally proposed by the authors policies and best practices, service/choreography goals, and so
is given as Linear Temporal Logic (LTL) formulas. Recently, on.
a further semantics in terms of the SCIFF Framework [2] Differently from procedural specifications, in which activi-
has been provided to ConDec [11]. Another contribution of ties can be inter-connected only by means of control-flow rela-
this work is the definition of a method for automatically tionships (sequence patterns, mixed with constructs supporting
perform the verification tasks, by exploiting the SCIFF-based the splitting/merging of control flows), the ConDec language
semantics, and its proof procedure. provides a number of control-independent abstractions to
In Section II we briefly introduce the ConDec language, constrain activities, alongside the more traditional ones. In
aimed to declarative describe open processes/services. Then in ConDec it is possible to insert past-oriented constraints, as
3
0..1
well as constraints that do not impose any ordering among accept 1-click payment send
register
advert payment done receipt
activities.
Furthermore, while procedural specifications are closed, i.e., 0..1
all what is not explicitly modeled is forbidden, ConDec models choose close standard payment
item order payment failure
are open: activities can be freely executed, unless they are
subject to constraints. This choice has two implications. First, Fig. 2. A ConDec model.
a ConDec model accommodates many different possible exe-
cutions, improving flexibility. Second, the language provides
abstractions to explicitly capture not only what is mandatory, optional constraints of CM.
but also what is forbidden. In this way, the set of possible
executions does not need to be expressed extensionally and
models remain compact. B. A ConDec Example
ConDec models do not impose a rigid scheduling of activ- Figure 2 shows the ConDec specification of a payment
ities; instead, they leave the services free to execute activities services. Boxes represent instances of activities. Numbers
in a flexible way, but respecting at the same time the imposed (e.g., 0; N..M) above the boxes are cardinality constraints
constraints. An execution trace, i.e. the set of the executed that tell how many instances of the activity have to be done
activities,we say that it is supported by a ConDec model (e.g., never; between N and M). Edges and arrows represent
if and only if it complies with all its constraints. Finally, relations( constraints) between activities. Double line arrows
it is important to note that well-defined ConDec models indicate alternate execution (after A, B must be done before
support only finite execution traces, because it must always A can be done again), while barred arrows and lines indicate
be guaranteed that a BP will eventually terminate. negative relations (doing A disallows doing B). Finally, a
ConDec has been mapped to two different underlying logic solid circle on one end of an edge indicates which activity
frameworks, providing two different semantics for the ConDec activates the relation associated with the edge. For instance,
constraints. Beside the originally proposed LTL mapping, in the execution of accept advert in Figure 2 does not activate
[11] a mapping to the SCIFF Framework has been proposed. any relation, because there is no circle on its end (a valid
SCIFF allows to define constraints in terms of the happening model could contain an instance of accept advert and nothing
of events and expectations about the happening or the non- else); activity register instead activates a relation with accept
happening of other events. Events can be partially specified, advert (a model is not valid if it contains only register).
by means of unbound variables. Possibly, such variables can If there is more than one circle, the relation is activated
be further constrained, a la CLP. E.g., it possible to say that if a by each one of the activities that have a circle. Arrows
certain event happens at time T , then another event is expected with multiple sources and/or destinations indicate temporal
to happen at a time T 0 with the CLP constraint T 0 > T . relations activated/satisfied by either of the source/destination
A simple ConDec model where activities a and b can be activities. The parties involved—a merchant, a customer, and
executed many times, but the execution of one automatically a banking service to handle the payment—are left implicit.
exclude the execution of the other, can be expressed in In our example, the six left-most boxes are customer actions,
SCIFF by means of two rules (Integrity Constraints, using the payment done/ payment failure model a banking service
SCIFF terminology): H(a, T ) ⇒ EN(b, T 0 ) and H(b, T ) ⇒ notification about the termination status of the payment
EN(a, T 0 )1 . Note that such a simple model, if expressed using action, and send receipt is a merchant action. If register
some procedural flow language such as for example Petri Nets, is done (once or more than once), then also accept advert
would lead to additional assumptions and choice points, thus must be done (before or after register) at least once. No
making the final model pointlessly complicated. temporal ordering is implied by such a relation. Conversely,
Formally, a ConDec model CM is composed by a set of the arrow from choose item to close order indicates that,
activities, which represent atomic units of work (i.e., units of if close order is done, choose item must be done at least
work associated to single time points, and relations among ac- once before close order. However, due to the barred arrow,
tivities, used to specify constraints on their execution. Optional close order cannot be followed by (any instance of) choose
constraints are also supported, to express preferable ways to item. The 0..1 cardinality constraints say that close order
interact, but allowing the possibility to violate them. and send receipt can be done at most once. 1-click payment
Definition 1 (ConDec model CM). A ConDec model is a must be preceded by register and by close order, whereas
triple hA, Cm , Co i, where: standard payment needs to be preceded only by close
order (registration is not required). After 1-click or standard
• A is a set of activities, represented as boxes containing
payment, either payment done or payment failure must
their name;
follow, and no other payment can be done, before either of
• Cm is a set of mandatory constraints;
payment done/failure is done. After payment done there
• Co is a set of optional constraints.
must be at most one instance of send receipt and before send
Given a ConDec model CM, notations ACM , Cm CM
and receipt there must be at least a payment done. Sample valid
CM
Co respectively denote the set of activities, mandatory and models are: the empty model (no activity executed), a model
1 The two rules state that if a Happens, then b is Expected Not to happen, containing one instance of accept advert and nothing else,
and viceversa. and a model containing 5 instances of choose item followed
4
by a close order. A model containing only one instance of have been composed. The two models are compatible, because
1-click payment instead is not valid. they both support the empty execution trace; therefore, by
carrying out solely a compatibility check would seem that a
III. C OMPATIBILITY AND L EGAL C OMPOSITION composition can be actually built. However, as soon as an
activity is executed, CM1 and CM2 are contradictory: both
In this section we address the problem of establishing if activity a and activity b can not be executed in the composite
some local models are compatible [12], i.e. if there exists an model. In the general case, if none of the local models contains
interaction trace allowed by the composed system. We first constraints which impose the execution of a certain activity
try to establish if a single model does indeed support at least (i.e., existenceN, exactlyN and choice constraints),
one interaction trace (i.e., it is conflict-free, and then we extend compatibility always returns a positive answer, because the
the notion to the composed system. Note that all the following empty execution trace is supported.
definitions are based on the idea of execution traces, i.e. on a
set of events (ground facts), happened at certain time point.
A. From Openness to Semi-Openness
First of all, we introduce the notion of ∃-entailment: the aim
is to define somehow when a model guarantees a property. Since a ConDec model is open, it implicitly allows the exe-
To do so, we look at the traces allowed by the local ConDec cution of activities not explicitly contained in the model itself.
model, and verify such property directly on the allowed traces. The following example clarifies the point. This characteristic
Once we move to verify a property on a trace, the semantic of could cause undesired compositions to be evaluated as correct,
the entailment symbol could be referred to the SCIFF semantic as in the following example.
(as we do), as well as to the LTL semantics. Example 2 (Composition and openness issues). A customer
Definition 2 (∃-entailment). A property Ψ is ∃-entailed by a wants to find a seller to interact with. The customer comes
ConDec model CM (CM |=∃ Ψ) if at least one execution with a ConDec model representing its own desired constraints
trace supported by CM entails the property as well. If that is and requirements. In particular, they express that:
the case, then one of the supported execution traces can be • the customer wants to receive a good from a seller;
interpreted as an example which proves the entailment. • if the customer pays for a good, then she expects that the
seller will deliver it;
Definition 3 (Conflict-free model [12]). A ConDec model • before paying, the customer wants the seller to provide a
CM is conflict-free iff it supports at least one possible ex- guarantee that the payment method is secure.
ecution trace, i.e., iff
Figure 3 shows the ConDec graphical models (CMC ) of the
CM |=∃ true customer and of three candidate sellers. The three sellers differ
for what concerns the possibility of emitting a guarantee upon
A conflicting model is an over-constrained model: it is request:
impossible to satisfy all its mandatory constraints at the same 1) the seller depicted in Figure 3(b) (CM1S ) explicitly states
time. that it does not provide any guarantee upon request;
Then we generalize the idea of conflict-freedom to the 2) the seller depicted in Figure 3(c) (CM2S ) explicitly
composed model: supports the possibility of providing a guarantee;
Definition 4 (Composite model [12]). Given n ConDec mod- 3) the seller depicted in Figure 3(d) (CM3S ) does not
els CMi = hAi , Cm
i
, Coi i , the composite model obtained by mention provide guarantee among its activities.
combining CM , . . . , CMn is defined as :
1 Following Definition 5 checking compatibility between CMC
n n n and the three candidate sellers would state that CMC is not
compatible with CM1S , but it is compatible with CM2S and
[ [ [
CM1 , . . . , CMn , h Ai , i
Coi i
COMP Cm ,
i=1 i=1 i=1 CM3S . In particular, the two compositions CMC ∪ CM2S
and CMC ∪ CM3S produce exactly the same global model.
Definition 5 (Compatibility). Two ConDec models CM1 and However, while the answer given for the first two compositions
CM2 are compatible if their composition is conflict-free, i.e., is in accordance with the intuitive notion of compatibility,
iff: the third one is not. In fact, when CMC is composed with
1 2
COMP CM , CM |=∃ true CM2S , the behaviour of the seller is modified in that also the
constraints of the customer must be respected. Contrariwise,
Obviously, the notion of compatibility can be generalized to
when the composition between CMC and CM3S is established,
the case of n local models. The detection of incompatibility
the local model of the customer has the effect of changing the
means that a sub-set of the n local models leads to a conflict.
local model of the seller, augmenting it with a new provide
note that checking compatibility could not be enough, as
guarantee activity. During the execution, the customer would
pointed out by the following example:
expect to receive a guarantee before paying, but this capability
Example 1 (Trivial compatibility). Two local models has not been mentioned by the seller in its local model, and
therefore there could be the case that it is not supported.
CM1 = a •−−I• b
2
The example clearly shows that the openness assumption
CM = a •−−
k−• b must be properly revised when dealing with the composition
5
c Seller Customer s1 Customer s2 Customer s3
1..*
send send send send
pay pay pay pay
good good good good
0
provide provide provide
guarantee guarantee guarantee
(a) Constraints of the customer. (b) Constraints of a seller (c) Constraints of a seller (d) Constraints of a seller
which does not provide guar- which is able to provide a guar- which does not explicitly deal
antees. antee. with the emission of a guaran-
tee.
Fig. 3. Local models of a customer and of three candidate sellers.
problem. To ensure that a composition can be established, • AO ↓plays , AO ∪ {(A, plays(Ri )) | Ri ∈
the obtained global model must obey to the following semi- dom(plays) ∧ (A, Ri ) ∈ AR};
openness requirement: for each involved party, the activities • AR ↓plays , AR/{(A, Ri ) |Ri ∈ dom(plays)};
under the responsibility of that party must also explicitly • Cm ↓plays and Co ↓plays are updated accordingly.
appear in its local model.
If AR ↓plays = ∅, each role has been substituted by a
concrete identifier and the model becomes ground. A legal
B. Augmenting ConDec Models with Roles and Participants composite ConDec can be now characterized as an augmented
In order to ensure the semi-openness assumption, each model obtained by composing a set of local models, each
activity must be associated to its corresponding originator or one grounded by taking into account the other ones, s.t. the
role. The following definition extends the basic definition of composition is ground.
a ConDec model with such a relationship. Definition 9 (Augmented composite model). Given a set of
Definition 6 (Augmented ConDec model). An augmented augmented local models Li = hIDi , AOi , ARi , Cm i
, Coi i (i =
ConDec model is a 4-tuple hAO, AR, Cm , Co i, where: 1, . . . , n) and a function plays mapping roles to identifiers,
• AO is a set of (A, O) pairs where A is an activity and
the composition of the local models w.r.t. plays is defined
O is its originator; as n
[
• AR is a set of (A, R) pairs where A is an activity and 1 n
COMP(L , . . . , L )plays = Li ↓plays
R represents the role of its originator; i=1
• Cm is a set of mandatory constraints over AO and AR;
where the union of two augmented models is a shortcut
• Co is a set of optional constraints over AO and AR.
representing the union of each corresponding element . A
If AR = ∅, the model is completely grounded. Contrariwise, composition is legal iff COMP(L1 , . . . , Ln )plays is ground (see
if AO = ∅ the model is abstract. Definition 6).
In this respect, a ConDec local model is defined as an aug- It is now possible to revise the notion of compatibility
mented model containing also an indication about the identifier reflecting also the semi-openness assumption.
of the local model, and where an activity is associated either
to such an identifier, or to an abstract role. Definition 10 (Strong compatibility). n local models
Li = hIDi , AOi , ARi , Cm i
, Coi i (i = 1, . . . , n) are strong
Definition 7 (Local augmented model). A ConDec local compatible under plays iff their augmented composition
augmented model is a 5-tuple hID, AO, AR, Cm , Co i, where: ∪
COMP(L1 , . . . , Ln )plays = hAO , AR , Cm
∪ ∪
, Co∪ i satisfies the
• ID is the identifier of the participant executing the local following properties:
model; 1 n
• COMP (L , . . . , L )plays is legal;
• the other elements retain the meaning of Definition 6; 1 n
• COMP (L , . . . , L )plays is conflict-free;
• AO is a set containing only elements of the type (A, ID). ∪
• for each (a, IDi ) which belongs to AO but does not
i
A role identifies a class of originators; in the composition belong to AO , it must hold that:
process, abstract roles employed in each local model are 1 n
COMP(L , . . . , L )plays |=∀ absence((a, IDi ))
mutually grounded to concrete local models which participate
to the composition. The third point states that if a certain activity a has been
associated to a participant IDi , but IDi has not explicitly
Definition 8 (Grounding of a model). Given an augmented
mentioned a in its specification, then the composition must
model CMaug = hAO, AR, Cm , Co i and a function plays
always ensure that a cannot be executed.
mapping roles to concrete identifiers (i.e., stating that a certain
identifier “plays” a given role), the grounding of CMaug Example 3. Let us re-examine the compatibility between the
on plays is obtained by substituting each role Ri with the local models of the customer and the second seller shown in
corresponding concrete participant identifier plays(Ri ): Figure 3, supposing that their identifiers are respectively alice
6
and hutter, and customer and seller represent their roles. In supported execution, while the strong approach requires to
the composition, alice plays the role of customer, and hutter guarantee that any execution supported by the composition
plays the role of seller. Hence, plays(alice) = customer respects the choreography.
and plays(hutter) = seller.
By adopting the definition of augmented models, the Con- Definition 11 (Weak conformance). A composition of local
Dec diagram of alice is: models COMP(L1 , . . . , Ln )plays is weak conformant with a
choreography Chor iff:
Lalice = h{(pay, alice)},
• L1 , . . . , Ln are strong compatible w.r.t. plays (see Def-
{(send good, seller), (provide guarantee, seller)},
{existenceN(1, (send good, seller)), . . .},
inition 10);
• COMP (L1 , . . . , Ln )plays |=∃ Chor ↓plays .
∅i
The grounding of alice w.r.t. the plays function is Definition 12 (Strong conformance). A composition of local
Lalice ↓plays = models COMP(L1 , . . . , Ln )plays is strong conformant with a
h{(pay, alice), (send good, hutter), (provide guarantee, hutter)},
choreography Chor iff:
• L1 , . . . , Ln are strong compatible w.r.t. plays (see Def-
∅,
{existenceN(1, (send good, hutter)), . . .}, inition 10);
• COMP (L1 , . . . , Ln )plays |=∀ Chor ↓plays .
∅i
Example 4 (Weak and strong conformance). Let us consider
The grounding of hutter is obtained in a similar way.
a simple (fragment of a) choreography involving two roles –
When the two local models are composed, the grounding of
a customer and a seller. The choreography states that:
alice causes (provide guarantee, hutter) to belong to the set
AO∪ of the composition. Since the execution trace provide 1) two possible payment methods are available to the
guarantee → pay → send good is compliant with the customer (payment by credit card and payment by cash);
composition but (provide guarantee, hutter) 6∈ AOhutter , 2) the customer can pay only after having closed the order;
the two local models are not strong compatible. 3) if the customer pays, then the seller is entitled to send
the ordered good and, conversely, a good is sent to the
customer only if a payment has been previously done.
IV. C ONFORMANCE TO A CHOREOGRAPHY
Figure 4 shows the ConDec model of the resulting choreog-
Once a global model has been obtained through the compo- raphy, and three possible local models which can be composed
sition step, and after a strong compatibility property has been to realize such a choreography. In particular, alice can play
verified, the application developer can move to further analise the role of Customer, while hutter and lewis can play the
the resulting system, trying to understand if it entails some role of Seller.
desired properties. Let us first consider the composition obtained by combining
We represent a choreography as an augmented abstract the model of alice with the one of lewis. The composition is
ConDec model (i.e., an augmented model associating all strong conformant with the choreography:
the activities to roles and not to concrete participants – see • The choreography allows an open choice on the payment
Definition 6). When realizing a choreography with a set of modality, and both local models only deal with payment
concrete local models, different possible errors may arise: by credit card.
• Conflicting composition: independently from the chore- • The combination of the constraints which relate the
ography, the chosen local models are not compatible. payment with the delivery of the good in the two
• Local non-conformance: a concrete local model is not local models leads to obtain the following constraint
able to correctly play, within the choreography, the role cc payment •−−I• send good , which is a
it has been assigned to. “specialization” of the choreography one (no choice is
• Global non-conformance: even if each single local model present).
is able to correctly play the role it has been assigned to, • alice states that before paying, she wants to close the
it could be the case that the global obtained model does order, and that between two payments at least one close
not conforms the choreography anymore. order must be executed; such a constraint is a special-
It could be also the case that a participant would not be able to ization of the simple precedence constraint contained
play the role it has been assigned to, but it would anyway be in the choreography.
able to take part to a conforming composition. Such a situation The composition obtained by combining the model of alice
may arise because when the constraints of each local model with the one of hutter is instead not strong conformant. In
are joint with the ones of the others, the constraints of the fact, hutter does not impose any temporal ordering between
participant could be correctly “completed”. the payment and the delivery of the good. Therefore, it could
As a consequence it is necessary to first check that the be possible that the good is sent twice: one time before the
composition is conflict-free, and then verify the whole compo- payment of alice, and another time afterwards. I.e., the follow-
sition against the choreography. To verify that a composition ing execution trace is supported by the composition: close
conforms to a desired choreography, two approaches can be order → send good → cc payment → send good. The
followed. The weak approach states that the composition must first execution of the send good activity is not preceded by
be consistent with the choreography constraints in at least one a payment, thus violating a prescription of the choreography.
7
alice Seller Customer lewis Customer hutter
1..*
Customer Seller
cc send cc send cc send
cc payment good payment good payment good
payment
close send
order good
close
cash
payment order
(a) A simple payment choreog- (b) Local model of alice. (c) Local model of lewis. (d) Local model of hutter.
raphy
Fig. 4. A simple choreography and three candidate local models (one customer and two sellers).
However, the composition is weak conformant, because it least one execution trace compliant with the model and the
supports different possible executions which comply with the property; such an execution trace can be considered as an
choreography. example proving the existential entailment of the property.
The case of |=∀ is reduced, similarly to model checking, to
V. V ERIFICATION THROUGH SCIFF the |=∃ of the complemented property; the generation of an
execution trace compliant with the model and the completed
The SCIFF framework has been originally developed for
property can be considered as a counter-example showing that
the declarative specification and run-time verification of inter-
the original property is not entailed by the model in all its
action protocols in the context of open Multi-Agent Systems
supported executions.
[2]. It features:
• A rule-based language for modeling all the constraints
that must be respected by the events characterizing the A. Compatibility Verification with g-SCIFF
executions of the system under study. These rules relate Let us briefly describe how g-SCIFF carries out the com-
the concepts of event occurrence with the one of ex- patibility verification between the customer’s model shown
pected/forbidden event, to model the (un)desired courses in Figure 3(a) and each one of the three sellers modeled
of interaction when a given situation is reached during in Figures 3(b)-(d). As we have seen, the constraints of a
the interaction. Events are modeled as logic programming composite model are obtained by joining all the constraints
terms (possibly containing variables), and are associated of the local models. Let us denote the composition of the
to an explicit execution/expected time; times and vari- customer’s model with each seller’s model with respectively
ables can be constrained by means of CLP constraints CMsc1 , CMsc2 and CMsc3 . The first step, according to Defi-
and Prolog predicates. nition 10, is to verify whether the composite model is legal;
• A clear declarative semantics characterizing the execution this is a syntactic test which can be trivially proven for all the
traces compliant with the modeled rules. three composite models: the role of Customer is grounded on
• A corresponding proof procedure, sound and complete c, and the role of Seller is respectively grounded on s1 , s2 and
w.r.t. the declarative semantics, which is able to dynami- s3 . The second and third step require instead the presence of a
cally acquire the events occurring during a specific execu- verifier able to prove conflict-freedom (|=∃ ) and to check if the
tion of the system, and check on-the-fly their compliance composite model meet the semi-openness requirement (|=∀ ).
with the modeled rules. When verifying the conflict-freedom of CMsc2 and CMsc3 , g-
In the last years, the framework has been applied in other SCIFF operates as follows:
contexts, such as clinical guidelines, business contracts and • it starts from the 1..∗ constraint on send good, generat-
processes, service choreographies [9]. In particular, a complete ing an occurrence of the event;
mapping of all the ConDec constraints in terms of SCIFF rules • this generated occurrence triggers the precedence (− −−I•)
has been provided, proving its soundness w.r.t. the original constraint involving send good and pay, leading to
ConDec semantics (specified by means of LTL formulae) and generate a previous payment;
discussing its impact on the verification techniques. • the generated payment, in turn, triggers the precedence
The SCIFF proof procedure has been then extended to deal (−−−I•) constraint involving pay and provide guar-
also with the static verification of interaction protocols. g- antee, leading to generate a previous emission of a
SCIFF is the generative variant of SCIFF devoted to this guarantee.
task: instead of checking if a given (partial or complete)
At the end of the verification process, the following sample
execution trace is compliant with the modeled rules, it is
execution trace is therefore produced by g-SCIFF: provide
able to generate compliant execution traces or to return a
guarantee → pay → send good 2 . When verifying the
negative answer if none exists [10]. In this way, g-SCIFF can
compatibility of CMsc1 , instead, after the third step g-SCIFF
be suitably exploited to effectively prove whether a ConDec
realizes that the execution of provide guarantee clashes with
model (translated to SCIFF) |=∃ or |=∀ a given property [9].
In particular, a ConDec model |=∃ a given property if and 2 The temporal relationships imposing the orderings between the three
only if the g-SCIFF proof procedure is able to generate at generated events are represented with CLP constraints
8
the 0 cardinality constraint (absence constraint) imposed by related to the possibility of introducing “soft” ConDec con-
s1 , and returns a negative answer attesting the incompatibility straints: currently, constraints are considered as hard, and not
of the local models. respecting one constraint leads to an incompatibility response.
The last requirement to be verified is that for each (a, IDi ) We are hypothesizing situations where behavioural interface
which belongs to CMsc2 /CMsc3 but does not belong to the specifications can also comprehend compensations actions and
corresponding local model, it must hold that the absence of explicit management of violations.
a is |=∀ by the composite model. In the case of CMsc2 , no
such activity actually exists, and therefore the requirement ACKNOWLEDGMENT
is directly met, attesting that the two local models are in- This work has been partially supported by the FIRB project
deed compatible. Contrariwise, CMsc3 contains the activity TOCAI.it (RBNE05BFRK) and by the Italian MIUR PRIN
(provide guarantee, s3 ) which is however not contained in 2007 project No. 20077WWCR8.
the local model of s3 . Therefore, g-SCIFF must prove whether
all execution traces compliant with the composite model do not R EFERENCES
contain the execution of the provide guarantee activity. As [1] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and
already pointed out, |=∀ is reduced to |=∃ by complementing M. Montali. An Abductive Framework for A-Priori Verification of Web
the property; in this specific case, the verification reduces to Services. In A. Bossi and M. J. Maher, editors, Proceedings of the 8th
International ACM SIGPLAN Conference on Principles and Practice of
check whether at least one execution trace compliant with the Declarative Programming, pages 39–50. ACM Press, 2006.
composite model exists s.t. at least one execution of provide [2] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and P. Tor-
guarantee is contained in the trace. The execution trace pro- roni. Verifiable Agent Interaction in Abductive Logic Programming: the
SCIFF framework. ACM Transactions on Computational Logic, 9(4),
vide guarantee → pay → send good, produced by g-SCIFF 2008.
when checking the conflict-freedom of CMsc3 , does satisfy the [3] T. Andrews, F. Curbera, H. Dholakia, Y. Goland, J. Klein, F. Leymann,
complemented property, and can be therefore considered as a K. Liu, D. Roller, D. Smith, S. Thatte, I. Trickovic, and S. Weerawarana.
Business Process Execution Language for Web Services, Version 1.1.
counter-example showing that the semi-openness requirement Standards proposal by BEA Systems, International Business Machines
is not met by the composite model, i.e., that c and s3 are not Corporation, and Microsoft Corporation, 2003.
compatible. [4] A. Barros, M. Dumas, and P. Oaks. A Critical Overview of the Web
Services Choreography Description Language (WS-CDL). BPTrends,
Finally, note that the conformance verification of a com- 2005.
posite model with a choreography is carried out by g-SCIFF [5] A. K. Chopra and C. P. Singh. Producing Compliant Interactions:
Conformance, Coverage, and Interoperability. In 4th International
similarly to the case of compatibility. In the case of strong Workshop on Declarative Agent Languages and Technologies IV (DALT
conformance, each constraint involved in the choreography is 2006), Selected, Revised and Invited Papers, volume 4327 of Lecture
complemented and then separately checked w.r.t. |=∃ . If at Notes in Computer Science, pages 1–15. Springer Verlag, 2006.
[6] E. Christensen, F. Curbera, G. Meredith, and S. Weerawarana. Web Ser-
least one complemented property is |=∃ , then the composition vices Description Language (WSDL) 1.1. http://www.w3.org/TR/wsdl,
is not strong conforming with the choreography. 2001.
[7] N. Kavantzas, D. Burdett, G. Ritzinger, T. Fletcher, and Y. Lafon.
Web Services Choreography Description Language Version 1.0, 2004.
VI. C ONCLUSIONS AND F UTURE W ORK http://www.w3.org/TR/ws-cdl-10/.
[8] M. Baldoni and C. Baroglio and A. Martelli and V. Patti. A Priori
In this paper we have address some issues related to the pro- Conformance Verification for Guaranteeing Interoperability in Open
cess of composing complex system by using existing compo- Environments. In A. Dan and W. Lamersdorf, editors, Proocedings of the
4th International Conference on Service-Oriented Computing (ICSOC
nents, in the context of the Service Oriented Architectures. Our 2006), volume 4294 of Lecture Notes in Computer Science. Springer
approach hypothesizes a bottom-up process in composing the Verlag, 2006.
global system, where the components are put together in order [9] M. Montali. Specification and Verification of Declarative Open Inter-
action Models: a Logic-Based Framework. PhD thesis, University of
to achieve some interaction, and choreography constraints are Bologna, 2009.
taken into account only at a second stage. Peculiarities of our [10] M. Montali, M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello,
solution are 1) the use of a open, declarative, logic based and P. Torroni. Verification from Declarative Specifications Using Logic
Programming. In M. G. D. L. Banda and E. Pontelli, editors, ICLP,
language to represent models of the services and also the number 5366 in LNCS, pages 440–454. Springer Verlag, 2008.
choreographies; 2) the exploit of the SCIFF Proof Procedure, [11] M. Montali, M. Pesic, W. M. P. van der Aalst, F. Chesani, P. Mello,
and in particular of the g-SCIFF proof, to automatically and S. Storari. Declarative Specification and Verification of Service
Choreographies. ACM Transactions on the Web - Accepted, 2009.
perform all the verification tasks; and 3) beside a yes/no [12] M. Pesic. Constraint-Based Workflow Management Systems: Shifting
answer, our approach provides as output also some interaction Controls to Users. PhD thesis, Beta Research School for Operations
trace that can be used to reason upon and analyse the global Management and Logistics, Eindhoven, 2008.
[13] M. Pesic and W. M. P. van der Aalst. A Declarative Approach for
system. Flexible Business Processes Management. In Proceedings of the BPM
This work is still in its preliminary stage, although some 2006 Workshops, volume 4103 of Lecture Notes in Computer Science,
successful experimental results have been already obtained. pages 169–180. Springer Verlag, 2006.
[14] W. M. P. van der Aalst, M. Dumas, A. H. M. ter Hofstede, N. Russell,
Future works will be devoted to better assess the theory behind H. M. W. Verbeek, and P. Wohed. Life After BPEL? In M. Bravetti,
the solution, and to provide a better comparison with other L. Kloul, and G. Zavattaro, editors, Proceedings of the 2nd International
approaches available in the literature, like [5], [8]. In particular, Workshop on Web Services and Formal Methods (WS-FM 2005), volume
3670 of Lecture Notes in Computer Science, pages 35–50. Springer
on the theme of the a-priori verification there is a huge research Verlag, 2005.
literature, as well as on the topic of reasoning on choreogra- [15] S. A. White. Business Process Modeling Notation Specification 1.0.
phies and roles. A further issue we intend to investigate is Technical report, OMG, 2006.