Method for the Specification, Composition, and Testing of Distributed Object Systems

摘要

The formation of a distributed system from a collection of individual components requires the ability for components to exchange syntactically well-formed messages. Several technologies exist that provide this fundamental functionality as well as the ability to locate components dynamically based on syntactic requirements. The formation of a correct distributed system requires, in addition, that these interactions between components be semantically well-formed. The method presented in this thesis is intended to assist in the development of correct distributed systems. We present a specification methodology based on three fundamental operators from temporal logic initially, next, and transient. From these operators we derive a collection of higher-level operators that are used for component specification. The novel aspect of our specification methodology is that we require that these operators be used in the following restricted manner. A specification statement can refer only to properties that are local to a single component. A single component must be able to guarantee unilaterally the validity of the specification statement for any distributed system of which it is a part.