On the Impact of Formal Methods in the SOA

We present an overview of recent research that provide a formal analysis of coordination and composition in Service Oriented Architectures. In particular we focus on transactional support in the Web Service Architecture. The classic notion of transaction in database systems evolved into weaker forms, in order to adapt to multi-domain, loosely coupled environments including the execution of long running activities. Despite the shared interest in these weaker transactions, supported by most languages for Web service coordination and composition, in many cases there is not an agreement on their semantics. Transactions are considered under two complementary perspectives. The former is the local perspective of the business process: transactions are a control construct providing a user-defined error handling mechanism. The latter, is the perspective addressing the synchronization among distributed services: distributed transaction protocols. Distributed transaction protocols are evolving according to the requirements of the real e-business scenario over the Web. One particular direction of this evolution, that we discuss, is the negotiation of service capabilities to enable automated selection.