Rewriting Semantics of Meta-Objects and
Composable Distributed Services
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 nd
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. We have been strongly influenced by the onion skin
model of actor reflection developed by Agha and his
collaborators which we
generalize and formalize in this paper within the framework of
rewriting logic.