Issue No. 08 - August (1994 vol. 20)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.310668
<p>Automated behavior analysis is a valuable technique in the development and maintenance of distributed systems. In this paper, we present a tractable dataflow analysis technique for the detection of unreachable states and actions in distributed systems. The technique follows an approximate approach described by Reif and Smolka, but delivers a more accurate result in assessing unreachable states and actions. The higher accuracy is achieved by the use of two concepts: action dependency and history sets. Although the technique does not exhaustively detect all possible errors, it detects nontrivial errors with a worst-case complexity quadratic to the system size. It can be automated and applied to systems with arbitrary loops and nondeterministic structures. The technique thus provides practical and tractable behavior analysis for preliminary designs of distributed systems. This makes it an ideal candidate for an interactive checker in software development tools. The technique is illustrated with case studies of a pump control system and an erroneous distributed program. Results from a prototype implementation are presented.</p>
distributed processing; software engineering; distributed systems; dataflow analysis; action dependency; history sets; worst-case complexity; pump control system; software development tools; arbitrary loops; nondeterministic structures; labeled transition systems; static analysis; program verification; distributed software engineering; synchronous communicating systems; reachability analysis
S. C. Cheung and J. Kramer, "Tractable Dataflow Analysis for Distributed Systems," in IEEE Transactions on Software Engineering, vol. 20, no. , pp. 579-593, 1994.