-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 an architectural paradigm for modeling and implement
ERVICE ORIENTED COMPUTING emerged recently as ing 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 [
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 [
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, 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 [
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 (b) Top-Down 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 [
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 [
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 [
II. MODELING A SERVICE BY MEANS OF THE CONDEC
LANGUAGE
ConDec is a declarative, graphical language proposed by
van der Aalst and Pesic [
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
[
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 0) and H(b; T ) ) EN(a; T 0)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. Definition 1 (ConDec model CM). A ConDec model is a triple hA; Cm; Coi, where:
A is a set of activities, represented as boxes containing their name; Cm is a set of mandatory constraints;
Co is a set of optional constraints.
Given a ConDec model CM, notations ACM, CmCM and CoCM respectively denote the set of activities, mandatory and 1The two rules state that if a Happens, then b is Expected Not to happen, and viceversa. accept advert choose item register 0..1 close order 1-click payment standard payment optional constraints of CM.
B. A ConDec Example payment done payment failure 0..1 send receipt
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 [
First of all, we introduce the notion of 9-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 (9-entailment). A property is 9-entailed by a
ConDec model CM (CM j=9 ) 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 [
CM j=9 true
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 [
COMP CM1; : : : ; CMn
n n n , h [ Ai; [ Cmi; [ Coi i i=1 i=1 i=1 Definition 5 (Compatibility). Two ConDec models CM1 and CM2 are compatible if their composition is conflict-free, i.e., iff:
COMP CM1; CM2 j=9 true
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 CM1 = 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, CM1 and CM2 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 (CMC ) 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) (CM1S ) explicitly states that it does not provide any guarantee upon request; 2) the seller depicted in Figure 3(c) (CM2S ) explicitly supports the possibility of providing a guarantee; 3) the seller depicted in Figure 3(d) (CM3S ) does not mention provide guarantee among its activities. Following Definition 5 checking compatibility between CMC and the three candidate sellers would state that CMC is not compatible with CM1S , but it is compatible with CM2S and CM3S . In particular, the two compositions CMC [ CM2S and CMC [ CM3S 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 CMC is composed with CM2S , the behaviour of the seller is modified in that also the constraints of the customer must be respected. Contrariwise, when the composition between CMC and CM3S 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 c pay 2 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.
Definition 6 (Augmented ConDec model). An augmented ConDec model is a 4-tuple hAO; AR; Cm; Coi, 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; Cm is a set of mandatory constraints over AO and AR; Co 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.
Definition 7 (Local augmented model). A ConDec local augmented model is a 5-tuple hID; AO; AR; Cm; Coi, where: ID is the identifier of the participant executing the local model; the other elements retain the meaning of Definition 6; AO is a set containing only elements of the type (A; ID).
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 = hAO; AR; Cm; Coi 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 Ri with the corresponding concrete participant identifier plays(Ri): AO #plays, AO [ f(A; plays(Ri)) j Ri dom(plays) ^ (A; Ri) 2 ARg; AR #plays, AR=f(A; Ri) jRi 2 dom(plays)g; Cm #plays and Co #plays are updated accordingly.
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.
Definition 9 (Augmented composite model). Given a set of augmented local models Li = hIDi; AOi; ARi; Cmi; Coi i (i = 1; : : : ; n) and a function plays mapping roles to identifiers, the composition of the local models w.r.t. plays is defined as n COMP(L1; : : : ; Ln)plays = [ i=1
i L #plays where the union of two augmented models is a shortcut representing the union of each corresponding element . A composition is legal iff COMP(L1; : : : ; Ln)plays is ground (see Definition 6).
It is now possible to revise the notion of compatibility reflecting also the semi-openness assumption.
Definition 10 (Strong compatibility). n local models i i Li = hIDi; AO ; AR ; Cmi; Coi i (i = 1; : : : ; n) are strong compatible under plays iff their augmented composition COMP(L1; : : : ; Ln)plays = hAO[; AR[; Cm[; Co[i satisfies the following properties:
COMP(L1; : : : ; Ln)plays is legal; COMP(L1; : : : ; Ln)plays is conflict-free; for each (a; IDi) which belongs to AO[ but does not belong to AOi, it must hold that:
COMP(L1; : : : ; Ln)plays j=8 absence((a; IDi)) The third point states that if a certain activity a has been associated to a participant IDi, but IDi 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 ConDec diagram of alice is:
Lalice = hf(pay; alice)g; f(send good; seller); (provide guarantee; seller)g; fexistenceN(1; (send good; seller)); : : :g; ;i
The grounding of alice w.r.t. the plays function is Lalice #plays= hf(pay; alice); (send good; hutter); (provide guarantee; hutter)g; ;; fexistenceN(1; (send good; hutter)); : : :g; ;i 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) 62 AOhutter, 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(L1; : : : ; Ln)plays is weak conformant with a choreography Chor iff:
L1; : : : ; Ln are strong compatible w.r.t. plays (see Definition 10);
COMP(L1; : : : ; Ln)plays j=9 Chor #plays.
Definition 12 (Strong conformance). A composition of local models COMP(L1; : : : ; Ln)plays is strong conformant with a choreography Chor iff:
L1; : : : ; Ln are strong compatible w.r.t. plays (see Definition 10);
COMP(L1; : : : ; Ln)plays j=8 Chor #plays.
Example 4 (Weak and strong conformance). Let us consider a simple (fragment of a) choreography involving two roles – a 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 I 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. close order
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
[
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 [
The SCIFF proof procedure has been then extended to deal
also with the static verification of interaction protocols.
gSCIFF 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 [
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 CMcs1 , CMcs2 and CMcs3 . 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 s1, s2 and s3. The second and third step require instead the presence of a verifier able to prove conflict-freedom (j=9) and to check if the composite model meet the semi-openness requirement (j=8). When verifying the conflict-freedom of CMcs2 and CMcs3 , gSCIFF operates as follows: it starts from the 1:: constraint on send good, generating an occurrence of the event; this generated occurrence triggers the precedence ( I ) constraint involving send good and pay, leading to generate a previous payment; the generated payment, in turn, triggers the precedence ( I ) 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 CMcs1 , instead, after the third step g-SCIFF realizes that the execution of provide guarantee clashes with 2The temporal relationships imposing the orderings between the three generated events are represented with CLP constraints the 0 cardinality constraint (absence constraint) imposed by s1, and returns a negative answer attesting the incompatibility of the local models.
The last requirement to be verified is that for each (a; I Di) which belongs to CMcs2 /CMcs3 but does not belong to the corresponding local model, it must hold that the absence of a is j=8 by the composite model. In the case of CMcs2 , no such activity actually exists, and therefore the requirement is directly met, attesting that the two local models are indeed compatible. Contrariwise, CMcs3 contains the activity (provide guarantee; s3) which is however not contained in the local model of s3. 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, j=8 is reduced to j=9 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 CMcs3 , 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 s3 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. j=9. If at least one complemented property is j=9, 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 [