Using Model Checking Techniques for Symbolic Synthesis of Distributed Programs

Abstract

Given the non-determinism and race conditions in distributed programs, the ability to provide assurance about them is crucial. Our work focuses on incremental synthesis where we modify existing "fault-intolerant" distributed programs to add fault-tolerance. We concentrate on reducing the complexity of such synthesis using techniques ?symmetry and parallelism? from model checking. We apply these techniques in the context of deadlock resolution. In particular, incremental synthesis requires removal of certain program actions that could violate safety in the presence of faults and such removal may eliminate all outgoing transitions from some states rendering them to be deadlock states. We focus on reducing the complexity of resolving such deadlock states using symmetry and/or parallelism. We show that these approaches provide a significant speedup separately as well as together.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2008
Accession Number
ADA488093

Entities

People

  • Borzoo Bonakdarpour
  • Fuad Abujarad
  • Sandeep S. Kulkarni

Organizations

  • Michigan State University

Tags

Communities of Interest

  • C4I
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Agreements
  • Algorithms
  • Boundaries
  • Case Studies
  • Cognitive Systems Engineering
  • Computations
  • Computer Science
  • Distributed Computing
  • Engineering
  • Fault Tolerance
  • Local Area Networks
  • Parallel Computing
  • Parallel Processing
  • Recovery
  • Specifications
  • Symmetry
  • Transitions

Fields of Study

  • Computer science

Readers

  • Parallel and Distributed Computing.
  • Systems Analysis and Design