ABSTRACT

We present a flow analysis technique for detecting unreachable states and actions in concurrent systems. It is an enhancement of the approach by Cheung and Kramer. Each process of a concurrent system is modeled as a finite state machine, whose states represent process execution states and whose transitions are labeled by actions. We construct dependency sets incrementally and eliminate spurious paths by checking the execution sequences of actions. We prove mathematically that our algorithm can detect more unreachability faults than the well-known Reif/Smolka and Cheung/Kramer algorithms. The algorithm is easy to manage and its complexity is still polynomial to the system size. Case studies on two commonly used communication protocols show that the technique is effective. Keywords: Concurrency; distributed systems; reachability analysis; static analysis

1. This research is supported in part by a grant of the Australian Research Council and a grant of the Research Grants Council of Hong Kong (Project No. 717308), 2. Centre for Software Analysis and Testing, Swinburne University of Technology, Hawthorn 3122, Australia. 3. China Merchants Bank, Central, Hong Kong. 4. Department of Computer Science, The University of Hong Kong, Pokfulam, Hong Kong. 5. (Corresponding author.) Department of Computer Science, The University of Hong Kong, Pokfulam, Hong Kong. Email:

EVERY VISITOR COUNTS: