|Information Sciences 194 (7): 254-269 (2012)|
T.Y. Chen 2 , Peifeng Hu 3 , Hao Li 4 and T.H. Tse 5
[paper from ScienceDirect | technical report TR-2012-01]
We present a flow analysis technique
for detecting unreachable states and actions in
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
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
|EVERY VISITOR COUNTS:|