CaltechTHESIS
  A Caltech Library Service

Applying Formal Methods to Distributed Algorithms Using Local-Global Relations

Citation

White, Jerome S. (2011) Applying Formal Methods to Distributed Algorithms Using Local-Global Relations. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/8FRW-ZF17. https://resolver.caltech.edu/CaltechTHESIS:05312011-123940546

Abstract

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.

Item Type:Thesis (Dissertation (Ph.D.))
Subject Keywords:local-global relations; distributed systems; formal methods
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
Thesis Committee:
  • Murray, Richard M. (chair)
  • Doyle, John Comstock
  • Martin, Alain J.
  • Holzmann, Gerard J.
  • Chandy, K. Mani
Defense Date:6 December 2010
Additional Information:Thesis title in 2011 Commencement program erroneously lists author's 2008 Master's thesis title as the PhD thesis title.
Record Number:CaltechTHESIS:05312011-123940546
Persistent URL:https://resolver.caltech.edu/CaltechTHESIS:05312011-123940546
DOI:10.7907/8FRW-ZF17
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:6481
Collection:CaltechTHESIS
Deposited By: Jerome White
Deposited On:06 Jun 2011 23:35
Last Modified:09 Oct 2019 17:11

Thesis Files

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

1MB

Repository Staff Only: item control page