Service Oriented Architectures are knowing a wide success, thanks to the maturity of standards and implementations. Moreover, the possibility of composing complex systems starting from simpler services is becoming supported by industrial tools, although still immature at the standard level. However, the a-priori verification aspect, i.e. the capability of determining before executing the system if it exhibits some particular behaviour, is still matter of an intense research effort.
In this paper we investigate the a-priori verification of bottomup build systems from the behavioural viewpoint, where a choreography is not known at the beginning of the developing process, but rather it is verified only later. We focus on the problem of deciding if, given a set of services, there can be some fruitful interaction among them; if yes, we focus also on the problem of determining such interaction. Our approach is based on specifying the services by means of the ConDec declarative language, and by exploiting its translation to the SCIFF Framework to automatically perform the verification task.
S ERVICE ORIENTED COMPUTING emerged recently as an architectural paradigm for modeling and implementing business collaboration within and across organizational boundaries. The Web Service technology, currently the most advanced implementation of Service Oriented Architecture (SOA) principles, is almost established as the standard technology for current business implementations, thanks to the support it has received from the academics as well as from the industrial partners.
A key aspect in the success of Service Oriented Computing (SOC) is the possibility of composing different, heterogeneous services, yet achieving a complex system starting from more simple components. Interoperability at the level of data exchange, as well as at the level of service location and invocation, has been guaranteed by standards like WSDL [6].
Industrial tools are becoming available to support also the composition process, too. Although languages for defining composition rules and models have been proposed, but none of them has enjoyed the maturity level of the other standards. Initial proposals like BPMN [15], WS-CDL [7] and BPEL [3] have been criticized for their intrinsic procedural nature, while the need for open, declarative approaches has been recognized only later [4], [14].
Automatic verification of properties regarding the behavioural aspects of the composed systems is deemed as a crucial step, but a comprehensive solution is lacking. Currently, DEIS -Department of Electronics, Informatics and Systems, University of Bologna. name.surname@unibo.it the task of ensuring that two services can successfully cooperate is demanded to the software architect that is designing the system. Analogously, ensuring that the composed system will exhibit certain properties is a task that directly burden the developer. Although such guarantees can be verified by human users with small systems, there are serious doubts of achieving such results when the composed systems grow in dimension and interaction complexity. Hence, the task of automatically verifying a service composition a-priori (during the designing phase), is of the fundamental importance to foster the service composition and the "off-the-shelf" composition model .
Several approaches have been adopted to address the verification of service composition. A very common way consist of checking one service against a global description of a system, like in [1], [8]. In order to succeed, the following assumptions are usually made: 1) there is a description of the whole system, from a global point of view; 2) there is 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 by the global specification (hence the global description can be 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 (also named choreography). The choreography is intended as a sort of "legal, tight contract", and plays a double role: it specifies the "boundaries" for the service under testing, and provides the expected behaviour of the other (unknown) peers. The obvious advantage of such approach is that the verification task involves only a service description and a choreography: the component "certified" as compliant can be then adopted to play a certain role within the global system, independently of the other peers.
In this paper we investigate the verification of service composition from another viewpoint. We start from the assumption that, at least in the beginning steps, a global choreography is not defined (or is not yet available). Beside a "top-down" developing method, where the developer starts designing the choreography and proceeds to refine the components in several steps, there is also a common "bottom-up" projecting style, where the developer simply starts to build up her application by putting together the already available components. If this is the case, the models of all parties (called local models thereafter) are directly composed, in order to make them interact and mutually benefit from each other, as in Figure 1a.
The first problem we try to address is: given a composition of services, does exist a successful interaction? If yes, how is made such interaction? In case of a positive answer to the first question, we say that the models are compatible. Beside the yes/no answer, we deem as fundamental also knowing as much as possible about such interactions. E.g., knowing in advance the supported interaction traces would help in the analysis of the global system features and properties. Of course, "compatible" does not mean that a successful interaction will be effectively achieved at run-time.
A second problem we discuss in this work is about choreographies, intended no more as a tight contract to be respected, but rather as a set of constraints representing the desired properties of the system. In this view, choreographies are not intended as the set of requirements each service should fulfill to interact, but rather a set of desired features that the global system will exhibit. Roughly, this problem can be formulated as follow: given a compatible set of services, does exists some successful interaction that honors the choreography constraints? If yes, how is made such interaction? Also in this case we aim to know not only a yes/no answer, but also some sort of fully/partially specified interaction trace.
In our approach, services and choreographies are represented by means of a declarative language, and in particular using the ConDec language [13]. We agree with the critics moved to procedural approaches in [4], [14]. In particular, choreographies (intended as a set of properties or constraints of the final resulting system) are more naturally represented in terms of declarative rules/constraints, rather than by sentences of a procedural language. In this work, we extend the original ConDec model to the concepts of roles, and provide definition of service composition compatibility on the resulting ConDec models.
The ConDec semantics originally proposed by the authors is given as Linear Temporal Logic (LTL) formulas. Recently, a further semantics in terms of the SCIFF Framework [2] has been provided to ConDec [11]. Another contribution of this work is the definition of a method for automatically perform the verification tasks, by exploiting the SCIFF-based semantics, and its proof procedure.
In Section II we briefly introduce the ConDec language, aimed to declarative describe open processes/services. Then in Section III and in Section IV we try to better capture the notion of compatible services (compatible models of services) and of compliance to a choreography. In Section V we show how such properties are automatically verified exploiting the ConDec Language and its translation into the SCIFF Framework [2]. Finally we conclude and discuss future works.
ConDec is a declarative, graphical language proposed by van der Aalst and Pesic [13] within the research field of Business Process Management (BPM). It aims to support specification, enactment and monitoring of Business Process, by means of constraints among activity executions. Constraints are declaratively expressed, as the authors claim that the adoption of a declarative approach fits better with complex, unpredictable processes, where a good balance between support and flexibility must be found. Although it has been originally proposed in the BPM context, it has been applied also in the far broader field of SOA. Former applications of ConDec regarded choreographies specification; in this paper, we adopt it to represent also service local models.
A ConDec model mainly consists of two parts: a set of activities, representing atomic units of work, and a set of relationships which constrain the way activities can be executed, and are therefore referred to as constraints. Constraints can be interpreted as policies/business rules, and may reflect different kinds of knowledge: external regulations and norms, internal policies and best practices, service/choreography goals, and so on.
Differently from procedural specifications, in which activities can be inter-connected only by means of control-flow relationships (sequence patterns, mixed with constructs supporting the splitting/merging of control flows), the ConDec language provides a number of control-independent abstractions to constrain activities, alongside the more traditional ones. In ConDec it is possible to insert past-oriented constraints, as well as constraints that do not impose any ordering among activities.
Furthermore, while procedural specifications are closed, i.e., all what is not explicitly modeled is forbidden, ConDec models are open: activities can be freely executed, unless they are subject to constraints. This choice has two implications. First, a ConDec model accommodates many different possible executions, improving flexibility. Second, the language provides abstractions to explicitly capture not only what is mandatory, but also what is forbidden. In this way, the set of possible executions does not need to be expressed extensionally and models remain compact.
ConDec models do not impose a rigid scheduling of activities; instead, they leave the services free to execute activities in a flexible way, but respecting at the same time the imposed constraints. An execution trace, i.e. the set of the executed activities,we say that it is supported by a ConDec model if and only if it complies with all its constraints. Finally, it is important to note that well-defined ConDec models support only finite execution traces, because it must always be guaranteed that a BP will eventually terminate.
ConDec has been mapped to two different underlying logic frameworks, providing two different semantics for the ConDec constraints. Beside the originally proposed LTL mapping, in [11] a mapping to the SCIFF Framework has been proposed. SCIFF allows to define constraints in terms of the happening of events and expectations about the happening or the nonhappening of other events. Events can be partially specified, by means of unbound variables. Possibly, such variables can be further constrained, a la CLP. E.g., it possible to say that if a certain event happens at time T , then another event is expected to happen at a time T with the CLP constraint T > T .
A simple ConDec model where activities a and b can be executed many times, but the execution of one automatically exclude the execution of the other, can be expressed in SCIFF by means of two rules (Integrity Constraints, using the SCIFF terminology): H(a, T ) ⇒ EN(b, T ) and H(b, T ) ⇒ EN(a, T ) 1 . Note that such a simple model, if expressed using some procedural flow language such as for example Petri Nets, would lead to additional assumptions and choice points, thus making the final model pointlessly complicated.
Formally, a ConDec model CM is composed by a set of activities, which represent atomic units of work (i.e., units of work associated to single time points, and relations among activities, used to specify constraints on their execution. Optional constraints are also supported, to express preferable ways to interact, but allowing the possibility to violate them.
• A is a set of activities, represented as boxes containing their name; optional constraints of CM.
Figure 2 shows the ConDec specification of a payment services. Boxes represent instances of activities. Numbers (e.g., 0; N..M) above the boxes are cardinality constraints that tell how many instances of the activity have to be done (e.g., never; between N and M). Edges and arrows represent relations( constraints) between activities. Double line arrows indicate alternate execution (after A, B must be done before A can be done again), while barred arrows and lines indicate negative relations (doing A disallows doing B). Finally, a solid circle on one end of an edge indicates which activity activates the relation associated with the edge. For instance, the execution of accept advert in Figure 2 does not activate any relation, because there is no circle on its end (a valid model could contain an instance of accept advert and nothing else); activity register instead activates a relation with accept advert (a model is not valid if it contains only register). If there is more than one circle, the relation is activated by each one of the activities that have a circle. Arrows with multiple sources and/or destinations indicate temporal relations activated/satisfied by either of the source/destination activities. The parties involved-a merchant, a customer, and a banking service to handle the payment-are left implicit.
In our example, the six left-most boxes are customer actions, payment done/ payment failure model a banking service notification about the termination status of the payment action, and send receipt is a merchant action. If register is done (once or more than once), then also accept advert must be done (before or after register) at least once. No temporal ordering is implied by such a relation. Conversely, the arrow from choose item to close order indicates that, if close order is done, choose item must be done at least once before close order. However, due to the barred arrow, close order cannot be followed by (any instance of) choose item. The 0..1 cardinality constraints say that close order and send receipt can be done at most once. 1-click payment must be preceded by register and by close order, whereas standard payment needs to be preceded only by close order (registration is not required). After 1-click or standard payment, either payment done or payment failure must follow, and no other payment can be done, before either of payment done/failure is done. After payment done there must be at most one instance of send receipt and before send receipt there must be at least a payment done. Sample valid models are: the empty model (no activity executed), a model containing one instance of accept advert and nothing else, and a model containing 5 instances of choose item followed by a close order. A model containing only one instance of 1-click payment instead is not valid.
In this section we address the problem of establishing if some local models are compatible [12], i.e. if there exists an interaction trace allowed by the composed system. We first try to establish if a single model does indeed support at least one interaction trace (i.e., it is conflict-free, and then we extend the notion to the composed system. Note that all the following definitions are based on the idea of execution traces, i.e. on a set of events (ground facts), happened at certain time point.
First of all, we introduce the notion of ∃-entailment: the aim is to define somehow when a model guarantees a property. To do so, we look at the traces allowed by the local ConDec model, and verify such property directly on the allowed traces. Once we move to verify a property on a trace, the semantic of the entailment symbol could be referred to the SCIFF semantic (as we do), as well as to the LTL semantics.
Definition 2 (∃-entailment). A property Ψ is ∃-entailed by a ConDec model CM (CM |= ∃ Ψ) if at least one execution trace supported by CM entails the property as well. If that is the case, then one of the supported execution traces can be interpreted as an example which proves the entailment.
Definition 3 (Conflict-free model [12]). A ConDec model CM is conflict-free iff it supports at least one possible execution trace, i.e., iff
A conflicting model is an over-constrained model: it is impossible to satisfy all its mandatory constraints at the same time.
Then we generalize the idea of conflict-freedom to the composed model: Definition 4 (Composite model [12]). Given n ConDec models CM i = A i , C i m , C i o , the composite model obtained by combining CM 1 , . . . , CM n is defined as :
Obviously, the notion of compatibility can be generalized to the case of n local models. The detection of incompatibility means that a sub-set of the n local models leads to a conflict. note that checking compatibility could not be enough, as pointed out by the following example:
Example 1 (Trivial compatibility). Two local models
have been composed. The two models are compatible, because they both support the empty execution trace; therefore, by carrying out solely a compatibility check would seem that a composition can be actually built. However, as soon as an activity is executed, CM 1 and CM 2 are contradictory: both activity a and activity b can not be executed in the composite model. In the general case, if none of the local models contains constraints which impose the execution of a certain activity (i.e., existenceN, exactlyN and choice constraints), compatibility always returns a positive answer, because the empty execution trace is supported.
Since a ConDec model is open, it implicitly allows the execution of activities not explicitly contained in the model itself.
The following example clarifies the point. This characteristic could cause undesired compositions to be evaluated as correct, as in the following example.
Example 2 (Composition and openness issues). A customer wants to find a seller to interact with. The customer comes with a ConDec model representing its own desired constraints and requirements. In particular, they express that:
• the customer wants to receive a good from a seller;
• if the customer pays for a good, then she expects that the seller will deliver it; • before paying, the customer wants the seller to provide a guarantee that the payment method is secure. Figure 3 shows the ConDec graphical models (CM C ) of the customer and of three candidate sellers. The three sellers differ for what concerns the possibility of emitting a guarantee upon request:
1) the seller depicted in Figure 3(b) (CM 1 S ) explicitly states that it does not provide any guarantee upon request; 2) the seller depicted in Figure 3(c) (CM 2 S ) explicitly supports the possibility of providing a guarantee; 3) the seller depicted in Figure 3(d) (CM 3 S ) does not mention provide guarantee among its activities. Following Definition 5 checking compatibility between CM C and the three candidate sellers would state that CM C is not compatible with CM 1 S , but it is compatible with CM 2 S and CM 3 S . In particular, the two compositions CM C ∪ CM 2
and CM C ∪ CM 3 S produce exactly the same global model. However, while the answer given for the first two compositions is in accordance with the intuitive notion of compatibility, the third one is not. In fact, when CM C is composed with CM 2 S , the behaviour of the seller is modified in that also the constraints of the customer must be respected. Contrariwise, when the composition between CM C and CM 3 S is established, the local model of the customer has the effect of changing the local model of the seller, augmenting it with a new provide guarantee activity. During the execution, the customer would expect to receive a guarantee before paying, but this capability has not been mentioned by the seller in its local model, and therefore there could be the case that it is not supported.
The example clearly shows that the openness assumption must be properly revised when dealing with the composition
provide guarantee (c) Constraints of a seller which is able to provide a guarantee.
(d) Constraints of a seller which does not explicitly deal with the emission of a guarantee. problem. To ensure that a composition can be established, the obtained global model must obey to the following semiopenness requirement: for each involved party, the activities under the responsibility of that party must also explicitly appear in its local model.
In order to ensure the semi-openness assumption, each activity must be associated to its corresponding originator or role. The following definition extends the basic definition of a ConDec model with such a relationship.
ConDec model is a 4-tuple AO, AR, C m , C o , where:
• AO is a set of (A, O) pairs where A is an activity and O is its originator; • AR is a set of (A, R) pairs where A is an activity and R represents the role of its originator; • C m is a set of mandatory constraints over AO and AR; • C o is a set of optional constraints over AO and AR. If AR = ∅, the model is completely grounded. Contrariwise, if AO = ∅ the model is abstract.
In this respect, a ConDec local model is defined as an augmented model containing also an indication about the identifier of the local model, and where an activity is associated either to such an identifier, or to an abstract role. A role identifies a class of originators; in the composition process, abstract roles employed in each local model are mutually grounded to concrete local models which participate to the composition. Definition 8 (Grounding of a model). Given an augmented model CMaug = AO, AR, C m , C o and a function plays mapping roles to concrete identifiers (i.e., stating that a certain identifier "plays" a given role), the grounding of CMaug on plays is obtained by substituting each role R i with the corresponding concrete participant identifier plays(R i ):
If AR ↓ plays = ∅, each role has been substituted by a concrete identifier and the model becomes ground. A legal composite ConDec can be now characterized as an augmented model obtained by composing a set of local models, each one grounded by taking into account the other ones, s.t. the composition is ground.
) and a function plays mapping roles to identifiers, the composition of the local models w.r.t. plays is defined as
where the union of two augmented models is a shortcut representing the union of each corresponding element . A composition is legal iff COMP(L 1 , . . . , L n ) plays is ground (see Definition 6).
It is now possible to revise the notion of compatibility reflecting also the semi-openness assumption.
• for each (a, ID i ) which belongs to AO ∪ but does not belong to AO i , it must hold that:
The third point states that if a certain activity a has been associated to a participant ID i , but ID i has not explicitly mentioned a in its specification, then the composition must always ensure that a cannot be executed.
Example 3. Let us re-examine the compatibility between the local models of the customer and the second seller shown in Figure 3, supposing that their identifiers are respectively alice and hutter, and customer and seller represent their roles. In the composition, alice plays the role of customer, and hutter plays the role of seller. Hence, plays(alice) = customer and plays(hutter) = seller.
By adopting the definition of augmented models, the Con-Dec diagram of alice is:
{(send good, seller), (provide guarantee, seller)}, {existenceN(1, (send good, seller)), . . .}, ∅
The grounding of alice w.r.t. the plays function is L alice ↓ plays = {(pay, alice), (send good, hutter), (provide guarantee, hutter)}, ∅, {existenceN(1, (send good, hutter)), . . .}, ∅
The grounding of hutter is obtained in a similar way.
When the two local models are composed, the grounding of alice causes (provide guarantee, hutter) to belong to the set AO ∪ of the composition. Since the execution trace provide guarantee → pay → send good is compliant with the composition but (provide guarantee, hutter) ∈ AO hutter , the two local models are not strong compatible.
Once a global model has been obtained through the composition step, and after a strong compatibility property has been verified, the application developer can move to further analise the resulting system, trying to understand if it entails some desired properties.
We represent a choreography as an augmented abstract ConDec model (i.e., an augmented model associating all the activities to roles and not to concrete participants -see Definition 6). When realizing a choreography with a set of concrete local models, different possible errors may arise:
• Conflicting composition: independently from the choreography, the chosen local models are not compatible. • Local non-conformance: a concrete local model is not able to correctly play, within the choreography, the role it has been assigned to. • Global non-conformance: even if each single local model is able to correctly play the role it has been assigned to, it could be the case that the global obtained model does not conforms the choreography anymore. It could be also the case that a participant would not be able to play the role it has been assigned to, but it would anyway be able to take part to a conforming composition. Such a situation may arise because when the constraints of each local model are joint with the ones of the others, the constraints of the participant could be correctly "completed".
As a consequence it is necessary to first check that the composition is conflict-free, and then verify the whole composition against the choreography. To verify that a composition conforms to a desired choreography, two approaches can be followed. The weak approach states that the composition must be consistent with the choreography constraints in at least one supported execution, while the strong approach requires to guarantee that any execution supported by the composition respects the choreography.
Definition 11 (Weak conformance). A composition of local models COMP(L 1 , . . . , L n ) plays is weak conformant with a choreography Chor iff:
• L 1 , . . . , L n are strong compatible w.r.t. plays (see Definition 10);
Definition 12 (Strong conformance). A composition of local models COMP(L 1 , . . . , L n ) plays is strong conformant with a choreography Chor iff:
• L 1 , . . . , L n are strong compatible w.r.t. plays (see Definition 10);
Example 4 (Weak and strong conformance). Let us consider a simple (fragment of a) choreography involving two rolesa customer and a seller. The choreography states that:
1) two possible payment methods are available to the customer (payment by credit card and payment by cash); 2) the customer can pay only after having closed the order; 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. Figure 4 shows the ConDec model of the resulting choreography, and three possible local models which can be composed to realize such a choreography. In particular, alice can play the role of Customer, while hutter and lewis can play the role of Seller.
Let us first consider the composition obtained by combining the model of alice with the one of lewis. The composition is strong conformant with the choreography:
• The choreography allows an open choice on the payment modality, and both local models only deal with payment by credit card. • The combination of the constraints which relate the payment with the delivery of the good in the two local models leads to obtain the following constraint cc payment •−− • send good , which is a "specialization" of the choreography one (no choice is present).
• alice states that before paying, she wants to close the order, and that between two payments at least one close order must be executed; such a constraint is a specialization of the simple precedence constraint contained in the choreography. The composition obtained by combining the model of alice with the one of hutter is instead not strong conformant. In fact, hutter does not impose any temporal ordering between the payment and the delivery of the good. Therefore, it could be possible that the good is sent twice: one time before the payment of alice, and another time afterwards. I.e., the following execution trace is supported by the composition: close order → send good → cc payment → send good. The first execution of the send good activity is not preceded by a payment, thus violating a prescription of the choreography. However, the composition is weak conformant, because it supports different possible executions which comply with the choreography.
The SCIFF framework has been originally developed for the declarative specification and run-time verification of interaction protocols in the context of open Multi-Agent Systems [2]. It features:
• A rule-based language for modeling all the constraints that must be respected by the events characterizing the executions of the system under study. These rules relate the concepts of event occurrence with the one of expected/forbidden event, to model the (un)desired courses of interaction when a given situation is reached during the interaction. Events are modeled as logic programming terms (possibly containing variables), and are associated to an explicit execution/expected time; times and variables can be constrained by means of CLP constraints and Prolog predicates. • A clear declarative semantics characterizing the execution traces compliant with the modeled rules. • A corresponding proof procedure, sound and complete w.r.t. the declarative semantics, which is able to dynamically acquire the events occurring during a specific execution of the system, and check on-the-fly their compliance with the modeled rules. In the last years, the framework has been applied in other contexts, such as clinical guidelines, business contracts and processes, service choreographies [9]. In particular, a complete mapping of all the ConDec constraints in terms of SCIFF rules has been provided, proving its soundness w.r.t. the original ConDec semantics (specified by means of LTL formulae) and discussing its impact on the verification techniques.
The SCIFF proof procedure has been then extended to deal also with the static verification of interaction protocols. g-SCIFF is the generative variant of SCIFF devoted to this task: instead of checking if a given (partial or complete) execution trace is compliant with the modeled rules, it is able to generate compliant execution traces or to return a negative answer if none exists [10]. In this way, g-SCIFF can be suitably exploited to effectively prove whether a ConDec model (translated to SCIFF) |= ∃ or |= ∀ a given property [9]. In particular, a ConDec model |= ∃ a given property if and only if the g-SCIFF proof procedure is able to generate at least one execution trace compliant with the model and the property; such an execution trace can be considered as an example proving the existential entailment of the property. The case of |= ∀ is reduced, similarly to model checking, to the |= ∃ of the complemented property; the generation of an execution trace compliant with the model and the completed property can be considered as a counter-example showing that the original property is not entailed by the model in all its supported executions.
Let us briefly describe how g-SCIFF carries out the compatibility verification between the customer's model shown in Figure 3(a) and each one of the three sellers modeled in Figures 3(b)-(d). As we have seen, the constraints of a composite model are obtained by joining all the constraints of the local models. Let us denote the composition of the customer's model with each seller's model with respectively CM s1 c , CM s2 c and CM s3 c . The first step, according to Definition 10, is to verify whether the composite model is legal; this is a syntactic test which can be trivially proven for all the three composite models: the role of Customer is grounded on c, and the role of Seller is respectively grounded on s 1 , s 2 and s 3 . The second and third step require instead the presence of a verifier able to prove conflict-freedom (|= ∃ ) and to check if the composite model meet the semi-openness requirement (|= ∀ ). When verifying the conflict-freedom of CM s2 c and CM s3 c , g-SCIFF operates as follows:
• it starts from the 1.. * constraint on send good, generating an occurrence of the event; • this generated occurrence triggers the precedence (− −− •) constraint involving send good and pay, leading to generate a previous payment; • the generated payment, in turn, triggers the precedence (− −− •) constraint involving pay and provide guarantee, leading to generate a previous emission of a guarantee. At the end of the verification process, the following sample execution trace is therefore produced by g-SCIFF: provide guarantee → pay → send good 2 . When verifying the compatibility of CM s1 c , instead, after the third step g-SCIFF realizes that the execution of provide guarantee clashes with the 0 cardinality constraint (absence constraint) imposed by s 1 , and returns a negative answer attesting the incompatibility of the local models.
The last requirement to be verified is that for each (a, ID i ) which belongs to CM s2 c /CM s3 c but does not belong to the corresponding local model, it must hold that the absence of a is |= ∀ by the composite model. In the case of CM s2 c , no such activity actually exists, and therefore the requirement is directly met, attesting that the two local models are indeed compatible. Contrariwise, CM s3 c contains the activity (provide guarantee, s 3 ) which is however not contained in the local model of s 3 . Therefore, g-SCIFF must prove whether all execution traces compliant with the composite model do not contain the execution of the provide guarantee activity. As already pointed out, |= ∀ is reduced to |= ∃ by complementing the property; in this specific case, the verification reduces to check whether at least one execution trace compliant with the composite model exists s.t. at least one execution of provide guarantee is contained in the trace. The execution trace provide guarantee → pay → send good, produced by g-SCIFF when checking the conflict-freedom of CM s3 c , does satisfy the complemented property, and can be therefore considered as a counter-example showing that the semi-openness requirement is not met by the composite model, i.e., that c and s 3 are not compatible.
Finally, note that the conformance verification of a composite model with a choreography is carried out by g-SCIFF similarly to the case of compatibility. In the case of strong conformance, each constraint involved in the choreography is complemented and then separately checked w.r.t. |= ∃ . If at least one complemented property is |= ∃ , then the composition is not strong conforming with the choreography.
In this paper we have address some issues related to the process of composing complex system by using existing components, in the context of the Service Oriented Architectures. Our approach hypothesizes a bottom-up process in composing the global system, where the components are put together in order to achieve some interaction, and choreography constraints are taken into account only at a second stage. Peculiarities of our solution are 1) the use of a open, declarative, logic based language to represent models of the services and also the choreographies; 2) the exploit of the SCIFF Proof Procedure, and in particular of the g-SCIFF proof, to automatically perform all the verification tasks; and 3) beside a yes/no answer, our approach provides as output also some interaction trace that can be used to reason upon and analyse the global system.
This work is still in its preliminary stage, although some successful experimental results have been already obtained. Future works will be devoted to better assess the theory behind the solution, and to provide a better comparison with other approaches available in the literature, like [5], [8]. In particular, on the theme of the a-priori verification there is a huge research literature, as well as on the topic of reasoning on choreographies and roles. A further issue we intend to investigate is related to the possibility of introducing "soft" ConDec constraints: currently, constraints are considered as hard, and not respecting one constraint leads to an incompatibility response. We are hypothesizing situations where behavioural interface specifications can also comprehend compensations actions and explicit management of violations.
This work has been partially supported by the FIRB project TOCAI.it (RBNE05BFRK) and by the Italian MIUR PRIN 2007 project No. 20077WWCR8.