CaltechAUTHORS
  A Caltech Library Service

Dynamic UNITY

Zimmerman, Daniel M. (2001) Dynamic UNITY. California Institute of Technology , Pasadena, CA. (Unpublished) http://resolver.caltech.edu/CaltechCSTR:2001.006

[img]
Preview
PDF - Submitted Version
See Usage Policy.

830Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:2001.006

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. <p> 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. <p> 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. <p> 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. <p> 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:Report or Paper (Technical Report)
Additional Information:© 2002 Daniel M. Zimmerman, California Institute of Technology. The research described in this thesis has been supported in part by grants from the Air Force Office of Scientific Research, the CISE Directorate of the National Science Foundation, the Center for Research in Parallel Computing, Parasoft, and Novell Corporation, and by an NSF Graduate Research Fellowship. I thank all these organizations for their support. This document was prepared in LATEX2ε, using a few publicly available macro packages and a few of my own. It was typeset directly to Adobe Portable Document Format on a PowerBook running Mac OS X, using the wonderful pdfTEX package as included in version 4.0 of MacTeX. I thank the author of CMacTeX, Thomas Kiffe, for his swift personal attention to my inquiries about the functionality and use of the software. The typeface used for the main text is Lucida Bright, the sans serif font is Lucida Sans, and the typewriter font is Lucida Sans Typewriter—all three designed by Bigelow & Holmes.
Group:Computer Science Technical Reports
Funders:
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)UNSPECIFIED
ParaSoft Inc.UNSPECIFIED
Center for Research in Parallel ComputingUNSPECIFIED
Novell CorporationUNSPECIFIED
NSF Graduate Research FellowshipUNSPECIFIED
Subject Keywords:distributed computing, formal methods, transition systems, UNITY
DOI:10.7907/Z9Q23X7V
Record Number:CaltechCSTR:2001.006
Persistent URL:http://resolver.caltech.edu/CaltechCSTR:2001.006
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:26922
Collection:CaltechCSTR
Deposited By: Imported from CaltechCSTR
Deposited On:12 Dec 2001
Last Modified:07 Mar 2017 18:06

Repository Staff Only: item control page