This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Tractable Dataflow Analysis for Distributed Systems
August 1994 (vol. 20 no. 8)
pp. 579-593

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.

[1] D. Callahan, K. Kennedy, and J. Subhlok, "Analysis of event synchronization in a parallel programming tool," inProc. Second ACM SIGPLAN Symp. Principles Practice Parallel Programming, Seattle, WA, Mar. 1990.
[2] S. C. Cheung and J. Kramer, "Enhancing compositional reachability analysis with context constraints," inProc. 1st ACM Int. Symp. Foundations of Software Eng. (ACM SIGSOFT), 1993, pp. 115-125.
[3] S. C. Cheung and J. Kramer, "Tractable flow analysis for anomaly detection in distributed programs, " inProc. 4th European Software Eng. Conf. (ESEC '93), 1993, pp. 283-300, published inLecture Notes in Comput. Sci. 717.
[4] S. C. Cheung and J. Kramer, "An integrated method for effective behavior analysis of distributed systems," inProc. 16th IEEE Int. Conf. Software Eng.(ICSE 16), Sorrento, Italy, May 1994.
[5] E. Duesterwald and M. L. Soffa, "Concurrency analysis in the presence of procedures using a data-flow framework," inProc. Symp. Testing, Analysis, and Verification (ACM SIGSOFT) (TAV4), 1991, pp. 36-48.
[6] S. Fischer, A. Scholz, and D. Taubner, "Verification in process algebra of the distributed control of track vehicles: A case study," inProc. 4th Int. Workshop on Comput.-Aided Verification CAV'92, 1992, pp. 192-205, published inLecture Notes in Comput. Sci. 663.
[7] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[8] K. Kennedy, "A survey of data flow analysis techniques," in S. S. Muchnicket al., Eds.,Program Flow Analysis--Theory and Applications. Englewood Cliffs, NJ: Prentice-Hall, 1981, pp. 5-54.
[9] J. Kramer, J. Magee, K. Ng, and M. Sloman, "The system architect's assistant for design and construction of distributed systems,"Proc. 4th Workshop on Future Trends of Distrib. Computing Syst., 1993, pp. 284-290.
[10] J. Krameret al., "CONIC: An integrated approach to distributed computer control systems,"IEE Proc., Part E, vol. 130, no. 1, pp. 1-10, Jan. 1983.
[11] D. Long and L. A. Clarke, "Data Flow Analysis of Concurrent Systems that use the Rendezvous Model of Synchronization," inProc. Symp. Testing, Analysis, and Verification (ACM SIGSOFT) (TAV4), 1991, pp. 21-35.
[12] S. P. Masticola and B. G. Ryder, "Static infinite wait anomaly detection in polynomial time," inProc. Int. Conf. Parallel Processing, vol. II, 1990, pp. 78-87.
[13] S. P. Masticola and B. G. Ryder, "A model of Ada programs for static deadlock detection in polynomial time," inProc. ACM/ONR Workshop on Parallel and Distrib. Debugging, Santa Cruz, CA, USA, 1991.
[14] C. E. McDowell and D. P. Helmbold, "Debugging concurrent programs,"ACM Comput. Surveys, vol. 21, no. 4, pp. 593-622, Dec. 1989.
[15] N. Mercouroff, "An algorithm for analyzing communicating processes," inProc. Mathematical Foundation of Programming Semantics '91, Pittsburgh, PA, USA, Mar. 1991, published inLecture Notes in Comput. Sci. 598.
[16] M. Nielsen, G. Plotkin, and G. Winskel, "Petri nets, event structures, and domains: Part I,"Theoretical Comput. Sci., vol. 13, pp. 85-108, 1981.
[17] J. Ostroff,Temporal Logic of Real-Time Systems. Research Studies Press, 1990.
[18] W. Peng and S. Purushothaman, "Toward data flow analysis of communicating finite state machines, " inProc. 8th ACM Symp. Principles of Distrib. Computing, Aug. 1989.
[19] W. Peng and S. Purushothaman, "Data flow analysis of communicating finite state machines,"ACM Trans. Programming Languages and Syst., vol. 13, pp. 399-432, 1991.
[20] A. Rabinovich, "Checking equivalences between concurrent systems of finite agents," inProc. 19th Int. Colloquium on Automata, Languages and Programming, 1992, pp. 696-707, published inLecture Notes in Comput. Sci. 623.
[21] J. Reif and S. Smolka, "Data flow analysis of distributed communicating processes,"Int. J. Parallel Programming, vol. 19, pp. 1-30, 1990.
[22] J. H. Reif, "Data flow analysis of communicating processes," inProc. 6th ACM Symp. Principles of Programming Languages, 1979, pp. 257-268.
[23] J. Reif and S. Smolka, "The complexity of reachability in distributed communicating processes,"Acta Informatica, vol. 25, no. 3, pp. 333-354, 1988.
[24] S. A. Smolka, "Analysis of communicating finite state processes," Ph.D. dissertation, Dep. Comput. Sci., Brown Univ., Providence, RI, Tech. Rep. No. CS-84-05, 1984.
[25] R. N. Taylor, "Complexity of analyzing the synchronization structure of concurrent programs,"Acta Informatica, vol. 19, pp. 57-84, 1983.
[26] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[27] R. N. Taylor and L. J. Osterweil, "Anomaly detection in concurrent software by static data flow analysis,"IEEE Trans. Software Eng., vol. SE-6, no. 3, pp. 265-278, 1980.
[28] R. D. Yang and C. G. Chung, "The analysis of infeasible concurrent paths of concurrent Ada programs," inProc. 14th Ann. Int. Comput. Software Applic. Conf. (COMPSAC 90), 1990, pp. 424-429.

Index Terms:
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
Citation:
Shing Chi Cheung, J. Kramer, "Tractable Dataflow Analysis for Distributed Systems," IEEE Transactions on Software Engineering, vol. 20, no. 8, pp. 579-593, Aug. 1994, doi:10.1109/32.310668
Usage of this product signifies your acceptance of the Terms of Use.