|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
 Digg  Furl  Spurl  Blink  Simpy  Google  Del.icio.us  Y!MyWeb | ||
| Search | ||
| ||
| ASCII Text | x | ||
| G.S. Avrunin, U.A. Buy, J.C. Corbett, L.K. Dillon, J.C. Wileden, "Automated Analysis of Concurrent Systems with the Constrained Expression Toolset," IEEE Transactions on Software Engineering, vol. 17, no. 11, pp. 1204-1222, November, 1991. | |||
| BibTex | x | ||
| @article{ 10.1109/32.106975, author = {G.S. Avrunin and U.A. Buy and J.C. Corbett and L.K. Dillon and J.C. Wileden}, title = {Automated Analysis of Concurrent Systems with the Constrained Expression Toolset}, journal ={IEEE Transactions on Software Engineering}, volume = {17}, number = {11}, issn = {0098-5589}, year = {1991}, pages = {1204-1222}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.106975}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - JOUR JO - IEEE Transactions on Software Engineering TI - Automated Analysis of Concurrent Systems with the Constrained Expression Toolset IS - 11 SN - 0098-5589 SP1204 EP1222 EPD - 1204-1222 A1 - G.S. Avrunin, A1 - U.A. Buy, A1 - J.C. Corbett, A1 - L.K. Dillon, A1 - J.C. Wileden, PY - 1991 KW - concurrent systems; constrained expression toolset; programming languages; reachable states; expression analysis techniques; source code; Ada-like design language; system traces; parallel programming; software tools VL - 17 JA - IEEE Transactions on Software Engineering ER - | |||
The constrained expression approach to analysis of concurrent software systems can be used with a variety of design and programming languages and does not require a complete enumeration of the set of reachable states of the concurrent system. The construction of a toolset automating the main constrained expression analysis techniques and the results of experiments with that toolset are reported. The toolset is capable of carrying out completely automated analyses of a variety of concurrent systems, starting from source code in an Ada-like design language and producing system traces displaying the properties represented bv the analysts queries. The strengths and weaknesses of the toolset and the approach are assessed on both theoretical and empirical grounds.
[1] G. M. Karam and R. J. Buhr, "Starvation and critical race analyzers for Ada,"IEEE Trans. Software Eng., vol. 16, pp. 829-843, Aug. 1990.
[2] S. M. Shatz and W. K. Cheng, "A Petri net framework for automated static analysis of Ada tasking behavior,"J. Syst. Software, vol. 8, pp. 343-359, 1988.
[3] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[4] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244-263, Apr. 1986.
[5] L. K. Dillon, "Verifying general safety properties of Ada tasking programs,"IEEE Trans. Software Eng., vol. 16, pp. 51-63, Jan. 1990.
[6] D. Helmbold and D. Luckham, "Debugging Ada tasking programs,"IEEE Software, vol. 2, pp. 47-57, Mar. 1985.
[7] Rosenblum, D.S., and D.C. Luckham, "Testing the Correctness of Tasking Supervisors with TSL Specifications," inProc. ACM SIGSoft 89 (Third Symp. Software Testing, Analysis, and Verification), No. TAV-3, 1989, pp. 187-196.
[8] J. C. Wileden, "Constrained expressions and the analysis of designs for dynamically-structured distributed systems," inProc. Int. Conf. on Parallel Process., Aug. 1982, pp. 340-344.
[9] 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.
[10] L. K. Dillon, G. S. Avrunin, and J. C. Wileden, "Constrained expressions toward broad applicability of analysis methods for distributed software systems,"ACM Trans. Program. Languages and Syst., vol. 10, pp. 374-402, July 1988.
[11] G. S. Avrunin, L. K. Dillon, and J. C. Wileden, "Experiments with automated constrained expression analysis of concurrent software systems," inProc. ACM SIGSOFT '89 3rd Symp. on Software Testing, Analysis and Verification, R. A. Kemmerer, Ed., pp. 124-130 (also published inSoftware Eng. Notes, vol. 14, no. 8, 1989).
[12] S. Katz and D. Peled, "An interleaving set temporal logic," inProc. 6th Ann. ACM Symp. on Principles of Distributed Comput., 1987, pp. 178-190.
[13] L. A. Clarke, J. C. Wileden, and A. L. Wolf, "Nesting in Ada programs is for the birds," inProc. ACM-SIGPLAN Symp. on the Ada Program. Language, 1980, pp. 139-145 (also published inSIGPLAN Notices, vol. 15, no. 11, 1980).
[14] R. J. Dakin, "A tree search algorithm for mixed integer programming problems,"Computer J., vol. 8, pp. 250-255, 1965.
[15] M. A. Saunders, "MINOS system manual," Dept. Operations Res., Stanford Univ., Palo Alto, CA, Tech. Rep. SOL 77-31, 1977.
[16] M. Young, R. N. Taylor, K. Forester, and D. Brodbeck, "Integrated concurrency analysis in a software development environment," inProc. ACM SIGSOFT '89 3rd Symp. on Software Testing, Analysis and Verification, R. A. Kemmerer, Ed., pp. 200-209 (also published inSoftware Eng. Notes, vol. 14, no. 8).
[17] S. Tu, S. M. Shatz, and T. Murata, "Theory and application of Petri net reduction for Ada-tasking deadlock analysis," preprint, 1990.
[18] K. C. Tai, "A graphical representation of rendezvous sequences of concurrent Ada programs,"ACM Ada Lett., vol. VI, no. 1, pp. 94-103, Jan./Feb. 1986.
[19] G. Ricart and A. K. Agrawala, "An optimal algorithm for mutual exclusion in computer networks,"Commun. ACM, vol. 24, pp. 9-17, 1981.
[20] L. Lamport, "A new solution of Dijkstra's concurrent programming problem,"Commun. ACM, vol. 17, no. 8, pp. 453-455, 1974.
[21] G. S. Avrunin and J. C. Wileden, "Describing and analyzing distributed software system designs,"ACM Trans. Program. Languages and Syst., vol. 7, pp. 380-403, July 1985.
[22] R. N. Taylor, "Complexity of analyzing the synchronization structure of concurrent programs,"Acta Inform., vol. 19, pp. 57-84, 1983.
[23] G. S. Avrunin, J. C. Corbett, L. K. Dillon, and J. C. Wileden, "Automated constrained expression analysis of real-time software," Dept. Comput. and Inform. Sci., Univ. Massachusetts, Amherst, Tech. Rep. 90-117, Dec. 1990.
[24] C. E. McDowell, "A practical algorithm for static analysis of parallel programs,"J. Parallel and Distributed Process., vol. 6, pp. 515-536, June 1989.
[25] A. Valmari, "A stubborn attack on state explosion," inComputer-Aided Verification '90(Series in Discrete Mathematics and Theoretical Computer Sci., vol. 3), E. M. Clarke and R. P. Kurshan, Eds. Providence, RI: Amer. Math. Soc., 1991, pp. 25-41.
[26] T. Murata, B. Shenker, and S. M. Shatz, "Detection of Ada static deadlocks using Petri net invariants,"IEEE Trans. Software Eng., vol. 15, pp. 314-326, Mar. 1989.