Title :
An incremental approach to reachability analysis of distributed programs
Author :
Tai, Kuo-Chung ; Koppol, Pramod V.
Author_Institution :
Dept. of Comput. Sci., North Carolina State Univ., Raleigh, NC, USA
Abstract :
We present an incremental approach to reachability analysis of distributed programs with synchronous communication and mailbox naming. Each process in a distributed program can be modeled as a communicating finite state machine (CFSM). A set of CFSMs is organized into a hierarchy. We present an algorithm that, for a given hierarchy of a set M of CFSMs, incrementally composes and reduces subsets of CFSMs in M. This incremental reachability analysis guarantees the detection of global deadlocks. We provide an algorithm for selecting a hierarchy for a set of CFSMs and show an incremental analysis of the gas station problem.
Keywords :
concurrency control; distributed processing; finite state machines; formal specification; systems analysis; communicating finite state machine; distributed programs; gas station problem; global deadlock detection; incremental analysis; mailbox naming; reachability analysis; synchronous communication; Algorithm design and analysis; Automata; Computer science; Concurrent computing; Discrete wavelet transforms; Electronic mail; Reachability analysis; Roentgenium; Safety; System recovery;
Conference_Titel :
Software Specification and Design, 1993., Proceedings of the Seventh International Workshop on
Print_ISBN :
0-8186-4360-9
DOI :
10.1109/IWSSD.1993.315504
