Problem statement

Mobile communication networks are often unstable since terminal devices can dynamically change the reachability status. Within service oriented architectures asynchronous service invocation is often the more suitable paradigm for the choreography and orchestration of mobile components. There is therefore a need to provide communication protocols that are able to manage asynchronous communication also in presence of unstable network connections. The formal modelling and analysis of these protocols is the first step towards the successful implementation and evaluation of reliable service-oriented applications.

Story

The particular issue we describe here has as main objective to define a variant of SOAP supporting asynchronous communications. The domain of the scenario is the definition of a SOAP-based protocol which supports asynchronous interactions, i.e., interactions different from the usual synchronous “request-response” interactions supported by the available SOAP implementations based on HTTP. Such kinds of interactions are quite relevant in the delivery of telecommunication services, as:

• service logic are triggered/activated by events produced, in an asynchronous way, by the network/special resources, or must react to such events during the execution of a service instance;
• requests produced by a service logic to a network/special resource may results in long computations (e.g., set-up of a call) which might also require the involvement of end-users;
• some service logic components may not be reachable (e.g., the ones deployed on mobile terminals), e.g., due to the temporary absence of communication.

• Backward compatibility:
• aSOAP must be compatible with SOAP v1.2 on HTTP;
• aSOAP have limited impact on the clients: i.e., the clients that do not need to support asynchronous interactions must be SOAP client, working according to a request-response mode; clients that need such a support should introduce limited variants w.r.t. normal SOAP requests;
• Reachability
• aSOAP must be able to deal with unreachability of the servers (e.g., due to lack of connectivity)
• aSOAP must be able to deal with the case where a server cannot return a response (either provisional or final) due to the lack of connectivity
• aSOAP must be able to deal with case where a response (either provisional or final) cannot be returned to a client due to the lack of connectivity
• Message Exchange Patterns
• aSOAP must be able to deal with requests that require the servers to perform some longduration processing (greater than HTTP time-out) before producing any results
• aSOAP must be able to deal with requests with multiple responses The protocol may rely on some intermediary nodes, which are assumed to be highly-available

Solution

We use formal methods and tools to model and verify the aSOAP design for safety/liveness properties. The intended behaviour of aSOAP has been described in various use-case scenarios in the form of message sequence charts, one for each such a scenario. These scenarios are then translated into an UML statechart diagrams. Currently these translations are done by hand, but algorithms are available to automate this process or verify that the resulting models conform the set of message sequence charts. Correctness properties are expressed in the logic mu-UCTL and the model checker UMC is used to verify these properties.

The advantage of this approach is that the design of the protocol can be validated before it is implemented.

Languages

• Message sequence charts
• UML statechart diagrams
• mu-UCTL and other logics

Tools

• UMC v3.3 or other model checkers

Steps

1. Create model in UML (UML case tool)
2. Formulate logic properties (in mu-UCTL or other logic)
3. Analyse model (UMC or other tool) w.r.t. properties
4. Create feedback at design level, before implementation

Relevant for Case Studies

• Telecom (shown)
• Automotive (to be shown)

Relevant for Work packages

• WP1: Modeling in Service-Oriented Architectures
• WP3: Qualitative Aspects of Services
• WP4: Quantitative Aspects of Services (to be seen)
• WP7: Model-driven Development (to be seen)

Papers