#Number
TR-PDS-1995-009

#Title
Observation and Verification of Software for Distributed Systems


#Author
Alexander I. Tomlinson

#Abstract
The main contribution of this dissertation is the development of new
theory and techniques in the areas of program observation and
verification.  These areas are important parts of the specification,
design, development and testing phases of a software project's
lifecycle.  Program observation involves formulating a query about the
behavior of a program and then monitoring the program as it executes in
order to determine the result of the query.  Observation is used in
the development phase to track down bugs and clarify understanding of
a program's behavior, and in the testing phase to ensure that a
program behaves as expected for a given input set.  Program
verification involves proving that a design meets its specification.
This is done during the design phase to ensure that the specifications
are satisfied.  The fundamental difference between observation and
verification is that observation applies to individual executions of a
program and verification applies to all executions.

Three observation systems are developed in this dissertation: global
functions, recursive logic (RCL), and DAG expressions.
%
  A global function has the form of a sum of local variables.  The
  observed program is monitored to determine if the value of the
  global function exceeds some constant.  Two special cases of this
  problem are considered.
%
  RCL is a recursive logic built upon conjunctive global predicates.
  Computational structures of common paradigms such as butterfly
  synchronization and distributed consensus can be expressed easily in
  RCL.
%
  DAG expressions are an extension of regular expressions from strings
  to directed acyclic graphs.  While a regular expression specifies
  patterns of letters in a string, a DAG expression specifies patterns
  of letters in a DAG.  The letters in a DAG expression represent local
  predicates.
%
Nonintrusive observation algorithms for each of these three systems
are developed, proven and analyzed for complexity.

A system for specifying and verifying distributed programs is
developed.  A new proof technique is also introduced which uses
induction on the complement of the causally precedes relation.  These
specification and verification techniques are demonstrated on two well
known algorithms (vector clocks and mutual exclusion) and one lesser
known algorithm (direct dependency clocks).

	
#Bib
@PhdThesis{Wald:PhD,
  author =       "Alexander I. Tomlinson",
  title =        "Observation and Verification of Software
	          for Distributed Systems",
  school =       "University of Texas at Austin, Dept. of
                  Electrical and Computer Engineering",
  address =      "Austin, TX",
  month =        aug,
  year =         "1995",
  note =	 "available via ftp or WWW at maple.ece.utexas.edu
		  as technical report TR-PDS-1995-009"
}