[Home] [CV] [Publications]

Publications

Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Rewriting Semantics of Distributed Meta Objects and Composable Communication Services
Denker, G. and Meseguer, J. and Talcott, C. L. - 1999

In distributed computing and in communications software there is a great interest in modular and composable approaches. In particular, services such as security or fault-tolerance and services intended for boosting performance that may in practice be “hard-wired” across different parts of the code of a distributed system should be treated in a much more modular way, so that they can be dynamically added to a system, and so that several such services can be composed to obtain their combined benefits. Besides the good software engineering reasons of thus making the systems much more easily reusable and adaptable, modularity and composability are also crucial at runtime, in the sense that some of these services, that may have a cost in performance, should not be used always and everywhere. Instead, they should be installed dynamically and selectively at runtime, in those areas or domains of the distributed system where they are needed in response to some security threat, failure, need for boosting performance, and so on. This paper proposes a semantic approach to make precise the reflective concept of composable service in a distributed system, and to reason about the properties of service compositions. Our approach is based on the executable formal semantics for distributed object-oriented systems provided by rewriting logic and explicitly addresses the reflective properties that are essential for having a truly modular notion of service. The formal model that we present seems promising not only for formal analysis and symbolic simulation, but also for the application of theorem proving methods to formally verify important properties of services and their compositions. Our model builds on the onion skin model of actor reflection developed by Agha and his collaborators. We illustrate the basic ideas with a case study treating communication services – fault-tolerance, encryption and authentication services – and their composition. Formal specification of service guarantees and combination of guarantees for composed services are also discussed.