
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
G.M. Karam, R.J.A. Buhr, "Temporal LogicBased Deadlock Analysis for Ada," IEEE Transactions on Software Engineering, vol. 17, no. 10, pp. 11091125, October, 1991.  
BibTex  x  
@article{ 10.1109/32.99197, author = {G.M. Karam and R.J.A. Buhr}, title = {Temporal LogicBased Deadlock Analysis for Ada}, journal ={IEEE Transactions on Software Engineering}, volume = {17}, number = {10}, issn = {00985589}, year = {1991}, pages = {11091125}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.99197}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Temporal LogicBased Deadlock Analysis for Ada IS  10 SN  00985589 SP1109 EP1125 EPD  11091125 A1  G.M. Karam, A1  R.J.A. Buhr, PY  1991 KW  temporal logicbased specification language; deadlock analyzer; Timebench; concurrent systemdesign environment; specification language; COL; lineartime temporal logic; formal basis; axiomatic reasoning; deadlock analysis tool; reasoning power; Ada designs; systemwide deadlockfree; theorem prover; deadlock algorithm; finite systems; worstcase computational complexity; Prolog; readers; writers; gas station; dining philosophers; layered communications system; Ada; computational complexity; inference mechanisms; logic programming; specification languages; system recovery; temporal logic VL  17 JA  IEEE Transactions on Software Engineering ER   
A temporal logicbased specification language and deadlock analyzer for Ada is described. The deadlock analyzer is intended for use within Timebench, a concurrent systemdesign environment with support for Ada. The specification language, COL, uses lineartime temporal logic to provide a formal basis for axiomatic reasoning. The deadlock analysis tool uses the reasoning power of COL to demonstrate that Ada designs specified in COL are systemwide deadlockfree: in essence, it uses a specialized theorem prover to deduce the absence of deadlock. The deadlock algorithm is shown to be decidable for finite systems and acceptable otherwise. It is also shown to have a worstcase computational complexity that is exponential with the number of tasks. The analyzer has been implemented in Prolog. Numerous examples are evaluated using the analyzer, including readers and writers, gas station, five dining philosophers, and a layered communications system. The results indicate that analysis time is reasonable for moderate designs in spite of the worstcase complexity of the algorithm .
[1] S. Agerwala, "Putting Petri nets to work,"IEEE Computer, vol. 12, no. 12, pp. 8594, Dec. 1979
[2] 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. 278292, Feb. 1986.
[3] G. S. Avrunin, U. A. Buy, J. C. Corbett, L. K. Dillon, and J. C. Wileden, "An automated analysis of concurrent systems with the constrained expression tool set," Dept. of Computer and Inform. Sci., Univ. Massachusetts, Amherst, Tech. Rep. 90116, Nov. 1990.
[4] R. Balzer, "A 15 year perspective on automatic programming,"IEEE Trans. Software Eng., vol. SE11, no. 11, pp. 12571268, Nov. 1985.
[5] M. BenAri, Z. Manna, and A. Pnueli, "The temporal logic of branching time," inProc. 8th Ann. ACM Symp. on Program. Languages(Williamsburg, VA), Jan. 1981.
[6] G. V. Bochmann, "Finite state descriptions of communication protocols,"Comput. Networks, vol. 2, pp. 361372, Oct. 1978.
[7] G. V. Bochmann, "Hardware specification with temporal logic: an example,"IEEE Trans. Computers, vol. C31, pp. 223231, Mar. 1982.
[8] D. Brand and P. Zafiropulo, "On communicating finite state machines,"J. ACM, vol. 30, no. 2, pp. 323342, Apr. 1983.
[9] R. J. A. Buhr,System Design with Ada. Englewood Cliffs, NJ: PrenticeHall, 1984.
[10] R. J. A. Buhr,Practical Visual Techniques for System Design. Englewood Cliffs, NJ: PrenticeHall, 1990.
[11] R. J. A. Buhr, G. M. Karam, C. J. Hayes, and C. M. Woodside, "Software CAD: a revolutionary approach,"IEEE Trans. Software Eng., vol. 16, pp. 235249, Mar. 1989.
[12] R. J. A. Buhret al., "Time Bench: a CAD tool for realtime system design," Dept. Syst. and Comput. Eng., Carleton University, Ottawa, ON, Can., Tech. Rep. SCE9017, Sept. 1990.
[13] A. R. Cavalli and L. Farinas Del Cerro, "A decision method for linear temporal logic," inProc. 7th Int. Conf. on Automated Deduction(Lecture Notes in Computer Science no. 170). New York: SpringerVerlag, 1984, pp. 113127.
[14] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic verification of finitestate concurrent systems using temporal logic,"ACM Trans. Program. Lang. Syst., vol. 8, no. 2, pp. 244263, Apr. 1986.
[15] W. F. Clocksin and C. S. Mellish,Programming in Prolog. New York: SpringerVerlag, 1984.
[16] P. J. Courtois, F. Heymans, and D. L. Parnas, "Concurrent control with readers and writers,"Commun. ACM, vol. 14, no. 2, pp. 667 668, Oct. 1971.
[17] H. M. Deitel,An Introduction to Operating Systems. Reading, MA: AddisonWesley, 1984.
[18] G. Estrin, R. S. Fenchel, R. R. Razouk, and M. K. Vernon, "SARA (System ARchitects Apprentice): Modeling, analysis, and simulation support for design of concurrent systems,"IEEE Trans. Software Eng., vol. SE12, no. 2, pp. 293311, Feb. 1986.
[19] F. C. Furtek, "Specification and verification of realtime, distributed systems using the theory of constraints," inProc. 5th Int. Conf. on Automated Deduction(Lecture Notes in Computer Science no. 87). New York: SpringerVerlag, 1980, pp. 110125.
[20] M. G. Gouda and C. K. Chang, "Proving liveness for networks of communicating finite state machines,"ACM Trans. Program. Languages and Syst., vol. 8, no. 1, pp. 154182, Jan. 1986.
[21] B. T. Hailpern,Verifying Concurrent Processes Using Temporal Logic(Lecture Notes in Computer Science no. 129). New York: SpringerVerlag, 1982.
[22] S. L. Hantler and J. C. King, "An introduction to proving the correctness of programs,"ACM Comput. Surveys, vol. 8, no. 3, pp. 331353, Sept. 1983.
[23] D. Helmbold and D. Luckham, "Debugging Ada tasking programs,"IEEE Software, vol. 2, pp. 4757, Mar. 1985.
[24] R. C. Holt, E. D. Lazowska, G. Scranaham, and M. A. Scott,Structured Concurrent Design with Operating System Applications. Reading, MA: AddisonWesley, 1978.
[25] G. M. Karam, "A toolset for temporal analysis in a design environment for concurrent systems," Ph.D. thesis, Dept. Systems and Comput. Eng., Carleton University, Ottawa, ON, Can., Tech. Rep. SCE872, Dec. 1986.
[26] G. M. Karam and R. J. A. Buhr, "Experience with the automatic temporal analysis of multitasking Ada designs," inProc. Int. Ada Conf., Boston, MA, Dec. 1987, pp. 3644.
[27] G. M. Karam and R. J. A. Buhr, "Starvation and critical race analyzers for Ada,"IEEE Trans. Software Eng., vol. 16, pp. 829843, Aug. 1990.
[28] R. Kowalski,Logic for Problem Solving. New York: NorthHolland, 1979.
[29] D. C. Luckham and F. W. Von Henke, "An overview of ANNA: a specification language for Ada,"IEEE Software, vol. 2, pp. 923, Mar. 1985.
[30] Z. Manna and A. Pnueli, "Verification of concurrent programs: the temporal framework," inThe Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. New York: Academic, 1981, pp. 215273.
[31] Z. Manna and A. Pnueli, "Verification of concurrent programs: temporal proof principles, " inLogics of Programs(Lecture Notes in Computer Science no. 131). New York: SpringerVerlag, 1981, pp. 200252.
[32] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: SpringerVerlag, 1980.
[33] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE7, pp. 417426, July 1981.
[34] V. Nguyen, D. Gries, and S. Owicki, "A model and temporal proof system for networks of processes," inProc. 12th Ann. Symp. on the Principles of Program, Languages(New Orleans, LA), Jan. 1985, pp. 121131.
[35] Owicki, S., and L. Lamport, "Proving Liveness Properties of Concurrent Programs,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455495.
[36] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223252, Sept. 1977.
[37] A. Pnueli and W. P. DeRoever, "Rendezvous with Adaa proof theoretic view," inProc. AdaTEC Conf. on Ada(Arlington, VA), Oct. 1982, pp. 129137.
[38] N. Rescher and A. Urquhart,Temporal Logic. New York: SpringerVerlag, 1971.
[39] W. E. Riddle and J. C. Wileden, "Languages for representing software specifications and designs,"ACM SIGSOFT Software Eng. Notes, Oct. 1978.
[40] D. Schwabe and A. R. Cavalli, "Temporal logic specification of a virtual ring LAN access protocol," inProc. 4th Workshop on Protocol Specification, verification and Testing(Skytop, PA), June 1984.
[41] R. L. Schwartz and P. M. MelliarSmith, "Temporal logic specifications of distributed systems," inProc. 2nd Int. Conf. on Distributed Syst. (Paris), Apr. 1981, pp. 446454.
[42] R. L. Schwartz and P. M. MelliarSmith, "From state machines to temporal logic: specification methods for protocol standards,"IEEE Trans. Commun., vol. COM30, pp. 24862496, Dec. 1982.
[43] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362376, May 1983.
[44] Reference Manual for the Ada Programming Language, U.S. Dept. Defense, Washington, DC, MILSTD1815a, 1983.
[45] P. Wolper, "Synthesis of communicating processes from temporal logic specifications," Ph.D. thesis, Dept. Comput. Sci., Stanford Univ., Palo Alto, CA, 1983.
[46] P. Zave and W. Schell, "Salient features of an executable specification language and its environment,"IEEE Trans. Software Eng., vol. SE12, no. 2, pp. 312325, Feb. 1986.