Record Details

Applying formal methods to distributed algorithms using local-global relations / Jerome White ; K. Mandy Chandy, advisor ; Richard M. Murray, committee chair
Pasadena, Calif. : California Institute of Technology, c2011
vii, 167 leaves : ill. (mostly col.) ; 28 cm
[CIT theses] ; 2011
"This thesis deals with the design and analysis of distributed systems in which homogeneous, autonomous agents collaborate to achieve a common goal. The class of problems studied includes consensus algorithms in which all agents eventually come to an agreement about a specific action. The thesis proposes a framework, called local-global, for analyzing these systems. A local interaction is an interaction among subsets of agents, while a global interaction is one among all agents in the system. Global interactions, in practice, are rare, yet they are the basis by which correctness of a system is measured. For example, if the problem is to compute the average of a measurement made separately by each agent, and all the agents in the system could exchange values in a single action, then the solution is straightforward: each agent gets the values of all others and computes the average independently. However, if the system consists of a large number of agents with unreliable communication, this scenario is highly unlikely. Thus, the design challenge is to ensure that sequences of local interactions lead, or converge, to the same state as a global interaction."
"The local-global framework addresses this challenge by describing each local interaction as if were a global one, encompassing all agents within the system. This thesis outlines the concept in detail, using it to design algorithms, prove their correctness, and ultimately develop executable implementations that are reliable. To this end, the tools of formal methods are employed: algorithms are modeled, and mechanically checked, within the PVS theorem prover; programs are also verified using the Spin model checker; and interface specification languages are used to ensure local-global properties are still maintained within Java and C# implementations. The thesis presents example applications of the framework and discusses a class of problems to which the framework can be applied."
Advisor and committee chair names found in the thesis' metadata record in the digital repository
Dissertation note:
Thesis (Ph. D.) -- California Institute of Technology, 2011
Bibliography, etc. note:
Includes bibliographical references (leaves 156-167). 100
Record appears in:

Options Library Call no Location Description Item type Status Due date
Offsite Storage THESIS Offsite storage c.1 Thesis Archival copy -


 Record created 2015-09-18, last modified 2016-11-02

Rate this document:

Rate this document:
(Not yet reviewed)