Using Model Checking Techniques for Symbolic Synthesis of Distributed Programs
MICHIGAN STATE UNIV EAST LANSING DEPT OF COMPUTER SCIENCE/ENGINEERING
Pagination or Media Count:
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 andor parallelism. We show that these approaches provide a significant speedup separately as well as together.
- Computer Programming and Software