This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Combining Static Concurrency Analysis with Symbolic Execution
October 1988 (vol. 14 no. 10)
pp. 1499-1511

Static concurrency analysis detects anomalous synchronization patterns in concurrent programs, but may also report spurious errors involving infeasible execution paths. Integrated application of static concurrency analysis and symbolic execution sharpens the results of the former without incurring the full costs of the latter when applied in isolation. Concurrency analysis acts as a path selection mechanism for symbolic execution, while symbolic execution acts as a pruning mechanism for concurrency analysis. Methods of combining the techniques follow naturally from explicit characterization and comparison of the state spaces explored by each, suggesting a general approach for integrating state-based program analysis techniques in a software development environment.

[1] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[2] K. R. Apt, "A static analysis of CSP programs," inProc. Workshop on Program Logic(Pittsburgh, PA), June 1983.
[3] Military Standard Ada Programming Language, ANSI/MIL-STD- 1815A-1983, American National Standards Institute, Jan. 1983.
[4] C. A. R. Hoare, "Communicating sequential processes,"Commun. ACM, vol. 21, pp. 666-677, 1978.
[5] F. Martin, "HAL/S--The avionics programming system for the shuttle," inProc. AIAA Conf. Comput. Aerospace, Los Angeles, CA, pp. 308-318, Nov. 1977.
[6] R. N. Taylor, "Complexity of analyzing the synchronization structure of concurrent programs,"Acta Informatica, vol. 19, pp. 57-84, 1983.
[7] L. A. Clarke, "A system to generate test data and symbolically execute programs,"IEEE Trans. Software Eng., vol. SE-2, pp. 215- 222, Sept. 1976.
[8] S. L. Hantler and J. C. King, "An introduction to proving the correctness of programs,"ACM Comput. Surveys, vol. 8, no. 3, pp. 331-353, Sept. 1983.
[9] L. A. Clarke and D. J. Richardson, "Symbolic evaluation--An aid to testing and verification," inSoftware Validation, H. Hausen, Ed. Amsterdam. The Netherlands: North-Holland, 1984, pp. 141- 166.
[10] J. C. Knight and V. S. Grine, "Symbolic execution of concurrent Ada programs," Dep. Comput. Sci., Univ. of Virginia, Charlottesville, VA, Tech. Rep., 1985.
[11] L. K. Dillon, "Verification of Ada tasking programs using symbolic execution, Part I: Partial correctness," Dep. Comput. Sci., Univ. Calif., Santa Barbara, CA, Tech. Rep. TRCS 87-20, Oct. 1987.
[12] L. K. Dillon, "Verification of Ada tasking programs using symbolic execution, Part II: General safety properties," Dep. Comput. Sci., Univ. Calif., Santa Barbara, CA, Tech. Rep. TRCS 87-21, Oct. 1987.
[13] R. N. Taylor, "Debugging real-time software in a host-target environment,"Technol. Sci. Inform., vol. 3, no. 4, pp. 281-288, 1984.
[14] J. L. Peterson,Petri Net Theory and the Modeling of Systems. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[15] 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.
[16] A. V. Aho, J. E. Hopcroft, and J. D. Ullman,The Design and Analysis of Computer Algorithms. Menlo Park, CA: Addison-Wesley, 1974.
[17] G. J. Holzmann, "Automated protocol validation in Argos: Assertion proving and scatter searching,"IEEE Trans. Software Eng., vol. SE-13, no. 6, pp. 683-696, June 1987.
[18] J. Pearl,Heuristics: Intelligent Search Strategies for Computer Problem Solving. Reading, Mass: Addison-Wesley, 1984.
[19] N. Nilsson,Principles of Artificial Intelligence. Palo Alto, CA: Tioga, 1980.
[20] T. E. Cheatham, Jr., G. H. Holloway, and J. A. Townley, "Symbolic evaluation and the analysis of programs,"IEEE Trans. Software Eng., vol. SE-5, pp. 402-417, July 1979.
[21] K. C. Tai and C. Y. Din, "Validation of concurrency in software specification and design," inProc. 3rd Int. Workshop Software Specification Des., Aug. 1985, pp. 223-227.
[22] M. Weiser, "Programmers use slices when debugging,"Commun. ACM, vol. 25, no. 7, pp. 446-452, July 1982.
[23] J. Bergeretti and B. Carre, "Information-flow and data-flow analysis of while-programs,"ACM Trans. Program. Lang. Syst., vol. 7, no. 1, pp. 37-61, Jan. 1985.
[24] W. E. Howden, "Symbolic testing and the DISSECT symbolic evaluation system,"IEEE Trans. Software Eng., vol. SE-3, pp. 266-278, July 1977.
[25] R. Boyer, B. Elspas, and K. Levitt, "SELECT--A formal system for testing and debugging programs by symbolic execution,"SIGPLAN Notices, vol. 10, no. 6, pp. 234-245, June 1975.
[26] J. C. King, "A new approach to program testing," inProc. of 1975 Int. Conf. Reliable Software, Los Angeles, CA, 1975.
[27] G. S. Avrunin, L. K. Dillon, J. C. Wileden, and W. E. Riddle, "Constrained expressions: adding analysis capabilities to design methods for concurrent software systems,"IEEE Trans. Software Eng., vol. SE- 12, pp. 278-292, Feb. 1986.
[28] J. L. Peterson and T. H. Bredt, "A comparison of models of parallel computation," inProc. IFIP 74, 1974, pp. 466-470.
[29] D. Mandrioli, R. Zicari, C. Ghezzi, and F. Tisato, "Modeling the Ada task system by Petri nets,"Comput. Lang., vol. 10, no. 1, 1985.
[30] E. T. Morgan, "Design and Analysis of Concurrent Software Systems," Ph.D. dissertation. Dep. Inform. Comput. Sci., Univ. Calif., Irvine, CA, 1986.
[31] E. T. Morgan and R. R. Razouk, "Interactive state-space analysis of concurrent systems,"IEEE Trans. Software Eng., vol. SE-13, pp. 1080-1091, Oct. 1987.
[32] M. Young, "How to leave out details: Error-preserving abstractions of state-space models," inProc. Second Workshop Software Testing, Anal., Verification, Banff, Alta., Canada, July 1988, Arcadia Doc. UCI-88-14, to appear.
[33] R. N. Taylor, "Analysis of concurrent software by cooperative application of static and dynamic techniques," inSoftware Validation, H. L. Hausen, Ed. Amsterdam: Elsevier Science, 1984, pp. 127-137.
[34] L. J. Osterweil, "Integrating the testing, analysis, and debugging of programs," inSoftware Validation, H. Hausen, Ed. Amsterdam, The Netherlands: North-Holland, 1984, pp. 73-102.
[35] R. N. Taylor, D. A. Baker, F. C. Belz, B. W. Boehm, L. Clarke, D. A. Fisher, L. Osterweil, R. W. Selby, J. C. Wileden, A. L. Wolf, and M. Young, "Next generation software environments: Principles, problems, and research directions," Dep. Inform. Comput. Sci., Univ. Calif., Irvine, CA, Tech. Rep. 87-16, July 1987; also issued as Arcadia Doc. UCI-87-10, Univ. Colorado Tech. Rep. CU-CS-370- 87, Univ. Mass., Amherst, Tech. Rep. 87-63, and Incremental Systems Corp. Tech. Rep. 87-7-1.

Index Terms:
program testing; static concurrency analysis; symbolic execution; synchronization patterns; concurrent programs; path selection mechanism; concurrency analysis; program analysis; software development environment; parallel programming; program testing
Citation:
"Combining Static Concurrency Analysis with Symbolic Execution," IEEE Transactions on Software Engineering, vol. 14, no. 10, pp. 1499-1511, Oct. 1988, doi:10.1109/32.6195
Usage of this product signifies your acceptance of the Terms of Use.