A Method for the Specification, Composition, and Testing of Distributed Object Systems
Creators: name: Sivilotti, Paolo A. G.
Publisher: name: California Institute of Technology
Year: 1998

description: 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: (i) A specification statement can refer only to properties that are local to a single component; (ii) 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. Specification statements that conform to these two restrictions we call certificates. The first restriction is motivated by our desire for these component specifications to be testable in a relatively efficient manner. In fact, we describe a set of simplified certificates that can be translated into a testing harness by a simple parser with very little programmer intervention. The second restriction is motivated by our desire for a simple theory of composition: If a certificate is a property of a component, that certificate is also a property of any system containing that component. Another novel aspect of our methodology is the introduction of a new temporal operator that combines both safety and progress properties. The concept underlying this operator has been used implicitly before, but by extracting this concept into a first-class operator, we are able to prove several new theorems about such properties. We demonstrate the utility of this operator and of our theorems by using them to simplify several proofs. The restrictions imposed on certificates are severe. Although they have pleasing consequences as described above, they can also lead to lengthy proofs of system properties that are not simple conjunctions. To compensate for this difficulty, we introduce collections of certificates that we call services. Services facilitate proof reuse by encapsulating common component interactions used to establish various system properties. We experiment with our methodology by applying it to several extended examples. These experiments illustrate the utility of our approach and convince us of the practicality of componentbased distributed system development. This thesis addresses three parts of the development cycle for distributed object systems: (i) the specification of systems and components, (ii) the compositional reasoning used to verify that a collection of components satisfy a system specification, and (iii) the validation of component implementations.
description: © 1998, Paolo A. G. Sivilotti, California Institute of Technology. 

Many people contributed to this research and I am thankful to them all. I have been fortunate to work with Mani Chandy, my academic advisor. His ability to extract the elegant solution hidden behind the ugly hack, or the clever insight camouflaged as a mundane question has been an inspiration. Many thanks also to the members of my thesis committee, Yaser Abu-Morstafa, Jim Arvo, Rajive Bagrodia, and Alain Martin, for taking the time to review this thesis and to make helpful suggestions. Thanks to other graduate students of our research group, past and present: John Thornley, Berna Massingill, Adam Rifkin, Eve Schooler, Rajit Manohar, Rustan Leino, Pete Carlin Joe Kiniry and Dan Zimmerman. Their individual influences shaped my research environment here at Caltech. Thanks also to Diane Goodfellow for her administrative support. Thanks to the friends who helped make the good times fun, and the less good times bearable. Especially John Thornley, for many interesting and entertaining discussions (some even related to research), and Mike Palmer, for being a beacon of sanity in a crazy world. To Linda Lowe a debt of gratitude, for her kindness and understanting. She has been my closest confident, telling me what I needed to hear and listening. She has been my closest confidant, telling me what I need to hear and listening to what I had to say. 

Finally, thanks to my family in particular, my parents, for their unwavering lode and support: Mass and Ruth, for making sure I always had a home; Marco, for encouraging my academic pursuits; and Katie, who has asked for so little and has given, me so much. This research has been funded in par by and IBM Computer Science Fellowship, and NSERC'67 Fellowship DARPA 
grant N00014-91-J-4014, the NSF under Cooperative Agreement no. CCR-91-20008 and AFORS grant F49620-94-1-0244.
description: Submitted - cstr1997.pdf
Submitted - postscript.ps