ArCo

EPSULon for Web Services

EPSULon is a tool intended for modeling and simulating distributed systems using the Interaction Systems Description Language (ISDL) notation. In particular, the tool can be used to design web services from different viewpoints and subsequently verify the consistency between these viewpoints. This page gives an example of this. It accompanies the technical report on "Service-oriented Design: A Multi-viewpoint Approach" that the reader can download from the publications page, along with more information on Service-Oriented Design.

This page first gives an example of a consistency relations between two viewpoints in service-oriented design and shows how the reader can verify this consistency in EPSULon. Subsequently, it explains some minor differences between the operators introduced in the technical report and the operators used in the tool. This should provide the reader with enough information to construct his or her own service oriented designs from different viewpoints and verify the consistency between these viewpoints.

Example

In the example, we verify the consistency of the behaviour of a single service provider to a choreography that describes the collaborative behaviour between a number of service providers to achieve a certain goal. Figure 1 shows the behaviour of a service provider and figure 2 shows the choreography in which the service provider participates.

The service provider behaviour describes the behaviour of the front office of an insurance company. The front office can receive a message that contains details about a required insurance (InsDetails). Upon receiving these details, it forwards them to the back office (InsDetailsFW). The back office can reply with one of two possible insurance options (InsOption1 and InsOption2) or with a notification that it failed to create a suitable insurance (InsOptionNone). If no suitable insurance could be created the front office replies to the client with a rejection notification (InsRejection), otherwise it replies with an offer (InsOffer). The client finalizes the insurance by explicitly requesting it (InsRequest). The insurance company then replies with details about the payment (InsPaymentDetails) and sends a thank-you-and-welcome-as-a-client note (InsThankYou).

The reader can simulate the provider behaviour by pressing the "play" button in the toolbar directly below the menu bar. If the reader presses the "play" button, the tool enters into simulation mode (recognizable by the "play" button being green). In simulation mode actions that can be performed are green. If they are green, we say that they are enabled. The reader can "perform" enabled actions by clicking on them (keep the mouse really still while clicking on them), the simulator will then "perform" the enabled action and calculate which actions are enabled next.

Remember to press the "stop" button when you are done simulating. The tool will stay in simulator mode as long as you have not pressed the "stop" button. It will even stay in the simulator mode when there are no more actions enabled.

The user can also obtain the trace-based semantics of the provider behaviour. The trace semantics enumerates the set of all possible (full) orderings of the interactions in which the provider can engage. To obtain the trace semantics of the service provider behaviour, select the "Relate" option in the "Tools" menu. In the window that appears type ["insbehavior"] and press enter (the name between the square brackets refers to the name that the service provider has in the project, as shown in the left frame). After typing this, the tool shows that there are three possible orderings of the interactions in which the service provider can engage. In the first ordering, the service provider receives insurance (InsDetails) and forwards them to the front office (InsDetailsFW). The front office then receives insurance option 1 (InsOption1) and send an offer to the client (InsOffer). The client then makes a request for the insurance to be finalized (InsRequest) and receives payment details (InsPaymentDetails) and a thank-you note (InsThankYou). The second ordering is the same as the first, but instead of receiving the first insurance option (InsOption1), the front office receives the second insurance option (InsOption2). In the third ordering, upon forwarding the insurance details (InsDetailsFW), the back office replies that it can not construct an insurance (InsOptionNone), which leads to a rejection to the client (InsRejection).

Figure 1. A Service Provider Behaviour

The choreography shows the collaborative behaviour between a number of service providers that has as its goal to create a suitable mortgage for a client. We will not go into detail about the exact behaviour of the choreography. It suffices to say that the service provider plays a role in the choreography (see the bottom-right part of the figure).

The reader can simulate the choreography and obtain its trace semantics by typing: ["choreography"]. Moreover, the reader can obtain the trace semantics of the role that the insurance service provider plays by restricting the choreography to that role. To this end type: restrict("choreography",{"InsuranceCompany"}). The same ordering will be shown more than once, because the tool does not perform any optimizations yet.

Figure 2. A Choreography

As the reader can see, the service provider behaviour has more interactions than the role that it plays in the choreography from figure 2. This is because the front office plays a role in another choreography that describes its collaboration with the back office. The interactions that are involved in that choreography are: InsDetailsFW, InsOption1, InsOption2, InsOptionNone. In addition to this the provider has an interaction that is not used in any choreography: InsThankYou.

To compare the service provider behaviour to the choreography, the interactions of the service provider that relate to another choreography must be abstracted from and the interactions that are not used at all must be removed. To this end we have two operators: abstract and remove. Try using them by typing: abstract(["insbehavior"],{"InsDetailsFW","InsOption1","InsOption2","InsOptionNone"}) or remove(["insbehavior"],{"InsThankYou"}). Both operations can be applied successively by typing: abstract(remove(["insbehavior"],{"InsThankYou"}),{"InsDetailsFW","InsOption1","InsOption2","InsOptionNone"}). The resulting provider behaviour can be compared to the role that the provider plays in the choreography (which was derived with the restrict operator as show above), using the equals relational operator: =. Hence, to verify whether the service provider conforms to the behaviour that the choreography prescribes for it, type (or rather copy): restrict("choreography",{"InsuranceCompany"})= abstract(remove(["insbehavior"],{"InsThankYou"}),{"InsDetailsFW","InsOption1","InsOption2","InsOptionNone"})

The example project can be downloaded as a zip file here. To use this project, unzip it first.

Differences between Operators from the Tool and the Technical Report

The tool supports the following operators.

[_]: String -> Behavior, [d] returns the trace-based semantics of design d, where d is identified by its name in the project. [d] in the tool corresponds to the Petri net of a design N_d in the technical report. However, the tool uses a trace-based semantics rather than a Petri net-based semantics.

restrict: String x Set -> Behavior, given a design d and a set of roles rs from that design, restrict(d,rs) returns the trace-based semantics of the joint behavior of those roles. The restrict operator corresponds to a composition of operators from the technical report. Specifically, restrict(d,rs) corresponds to (N_d \ (subnet(rs) intersection T_d)). Again, the restrict operator returns a trace-based instead of a Petri net-based semantics.

=: Behavior x Behavior -> Bool, b1 = b2 returns true iff b1 is trace equivalent to b2. In the technical report the equivalence relation is based on branching bi-similarity of Petri nets instead of trace equivalence and the symbol ~ is used instead of the symbol =.

actions: String -> Set, actions(d) returns the set of all actions in design d. Actions in the tool correspond to internal tasks in the technical report. Internal tasks are obtained using IT_d.

interactioncontributions: String -> Set, interactioncontributions(d) returns the set of all interaction contributions in design d. Interaction contributions in the tool correspond to events in the technical report. Events are obtained using E_d. The tool does not distinguish between send and receive events.

abstract: Behavior x Set -> Behavior, abstract(b,s) returns the behavior derived from b in which all (inter)actions from s are abstracted from. abstract(b,s) in the tool corresponds to sigma(b,s) in the technical report, but abstract operates on traces, while sigma operates on Petri nets.

remove: Behavior x Set -> Behavior, remove(b,s) returns the behavior derived from b in which all (inter)actions from s are removed. remove(b,s) in the tool corresponds to rho(b,s) in the technical report, but abstract operates on traces, while rho operates on Petri nets.

join: Behavior x Behavior -> Behavior, join(b1,b2) returns the join of b1 and b2. join(b1,b2) in the tool corresponds to b1 cross _{{(e1, e2) | (e1, e2) in Ed1 x Ed2, e1=e2}} b2, where d1 and d2 are the designs from which b1 and b2 are the behavioural semantics respectively. Note that the join operator in the tool does not allow for the specification of the interactions by which the behaviours communicate. Instead, the tool assumes that if two events have the same name, they are meant to form an interaction.

in: String x Set -> Set, given a design d and a set of roles rs from that design in(d,rs) returns the set of interactions between these roles. in(d,rs) in the tool corresponds to IN_d(rs) in the technical report.

The set operators are not different from the regular set operators, except for their notation which has been tailored to be easy to enter into the tool. The set operators supported by the tool are the following:

{_, _, ...}: String x String x ... -> Set, returns the set consisting of the given strings.

U: Set x Set -> Set, s1 U s2 returns the union of s1 and s2.

^: Set x Set -> Set, s1 ^ s2 returns the common elements of s1 and s2.

-: Set x Set -> Set, s1 - s2 returns the s1 minus s2.

The mark operator from the technical report is not supported in the tool. If two or more instances of the same role are used in the tool, they have to identified and named explicitly (refer to the ISDL homepage for an explanation on how to do this).