Open distributed systems (ODS) exhibit a high degree of dynamicity and autonomy. ODS evolve dynamically and components of ODS interact with an environment that is not under their control. A wide range of protocols and activities must be composed to implement end-to-end distributed application management. These protocols and activities must execute concurrently, non-disruptively and share the same resources. In order to avoid resource conflicts, deadlocks, inconsistencies and incorrect execution semantics, the underlying resource management system must ensure that the simultaneous system activities compose in a correct manner. The difficulty in reasoning about system level interactions is due to the complexity of characterizing the semantics of shared resources and specifying what correctness of the overall system means. In this paper, we develop a mathematical framework and formal mechanisms for reasoning about the interaction and composition of resource management activities in open distributed systems, their dynamic installation and modification. In particular, we develop a two-level meta-architectural model of distributed computation based on Actors, a model of concurrent objects. The utility of this model is illustrated by developing specification of resource management services – remote creation, migration and reachability snapshot, and reasoning about their composability.
Keywords: distributed computation, resource management, meta-architecture, composition, specification, verification