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

fYear

1993

fDate

6-7 Dec 1993

Firstpage

141

Lastpage

150

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Specification and Design, 1993., Proceedings of the Seventh International Workshop on

Print_ISBN

0-8186-4360-9

Type

conf

DOI

10.1109/IWSSD.1993.315504

Filename

315504