The specification of distributed objects: liveness and locality
Paolo A. G. Sivilotti, Charles P. Giles · Conference of the Centre for Advanced Studies on Collaborative Research · 1999
There are two aspects to the behavioral specification of an object in a distributed system: safety and liveness. This paper describes our component-based mechanism for specifying liveness. The specification of a distributed object is typically a syntactic definition of its interface (e.g., the method signatures). Several proposals exist for extending these syntactic definitions to provide behavioral information (e.g., preconditions and postconditions). However, many of these proposals have failed to address liveness properties. In this paper, we argue for the need to express such properties. Our approach is a simple extension of CORBA IDL. Our extension is guided by the design-by-contract philosophy of sequential systems. In particular, our approach is consistent with testing for contract violations and debugging. These activities are critical for the practical use of any specification methodology in real systems.