CaltechTHESIS
  A Caltech Library Service

Dynamic UNITY

Citation

Zimmerman, Daniel M. (2002) Dynamic UNITY. Dissertation (Ph.D.), California Institute of Technology. http://resolver.caltech.edu/CaltechETD:etd-12072001-160019

Abstract

Dynamic distributed systems, where a changing set of communicating processes must interoperate to accomplish particular computational tasks, are becoming extremely important. Designing and implementing these systems, and verifying the correctness of the designs and implementations, are difficult tasks. The goal of this thesis is to make these tasks easier.

This thesis presents a specification language for dynamic distributed systems, based on Chandy and Misra's UNITY language. It extends the UNITY language to enable process creation, process deletion, and dynamic communication patterns.

The thesis defines an execution model for systems specified in this language, which leads to a proof logic similar to that of UNITY. While extending UNITY logic to correctly handle systems with dynamic behavior, this logic retains the familiar UNITY operators and most of the proof rules associated with them.

The thesis presents specifications for three example dynamic distributed systems to demonstrate the use of the specification language, and full correctness proofs for two of these systems and a partial correctness proof for the third to demonstrate the use of the proof logic.

The thesis details a method for determining whether a system in the specification language can be transformed into an implementation in a standard programming language, as well as a method for performing this transformation on those specifications that can. This guarantees a correct implementation for any specification that can be so transformed.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:distributed computing; formal methods; program specification; transition systems; UNITY
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Chandy, K. Mani (advisor)
  • Hickey, Jason J. (co-advisor)
Thesis Committee:
  • Chandy, K. Mani (chair)
  • Martin, Alain J.
  • Hickey, Jason J.
  • Bruck, Jehoshua
Defense Date:27 July 2001
Author Email:dmz (AT) cs.caltech.edu
Record Number:CaltechETD:etd-12072001-160019
Persistent URL:http://resolver.caltech.edu/CaltechETD:etd-12072001-160019
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:4821
Collection:CaltechTHESIS
Deposited By: Imported from ETD-db
Deposited On:10 Dec 2001
Last Modified:26 Dec 2012 03:12

Thesis Files

[img]
Preview
PDF (thesis-online.pdf) - Final Version
See Usage Policy.

830Kb

Repository Staff Only: item control page