The signal calculus: beyond message based coordination for services

This thesis aims at the definition of foundational techniques driving the design and implementation of a programming middleware supporting the full adoption of a MDD framework for Service Oriented Computing. Our main contribution is the definition of a compositional model for services in the spirit of choreography. Our model takes the form of two-level process calculus that lays at two different levels of abstraction. The local view of coordination is represented by the Signal Calculus, which is tailored to support the formal design of services. The global view of the coordination is supported by the Network Coordination Policies Calculus. The Network Coordination Policies Calculus is the formal machinery we introduced to specify choreography. Distinguished features of our approach are given by the adoption of the event notification paradigm as basic mechanisms to manage service interactions and by the usage of multicast communication. To fill the gap between the local and global views, we relate the semantics of the two calculi by a correctness result that allows us to verify if a design respects a specification. Finally, to highlight the benefit of our approach, we address the issue of defining Long Running Transactions via the Signal Calculus and we provide some sound refactoring rules in the spirit of the MDD approach to software design. The main advantage of these results consists in guaranteeing that the designer can refine the reference implementation without altering the intended meaning.