An action/state-based model-checking approach for the analysis of an asynchronous protocol for Service-Oriented Applications?

In this paper we present an action/state-based logical frame- work for the analysis and verication of complex systems, which relies on the denition of doubly labelled transition systems. The dened tempo- ral logic, called UCTL, combines the action paradigm|classically used to describe systems using labelled transition systems|with predicates that are true over states|as captured when using Kripke structures as semantic model. An ecient model checker for UCTL has been realized, exploiting an on-the-y algorithm. We then show how to use UCTL and its model checker in the design phase of an asynchronous extension of SOAP, called aSOAP. For this purpose, we describe aSOAP as a set of communicating UML state machines, for which a semantics over doubly labelled transition systems has been provided.