This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Temporal Logic-Based Deadlock Analysis for Ada
October 1991 (vol. 17 no. 10)
pp. 1109-1125

A temporal logic-based specification language and deadlock analyzer for Ada is described. The deadlock analyzer is intended for use within Timebench, a concurrent system-design environment with support for Ada. The specification language, COL, uses linear-time 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 deadlock-free: 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 worst-case 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 worst-case complexity of the algorithm .

[1] S. Agerwala, "Putting Petri nets to work,"IEEE Computer, vol. 12, no. 12, pp. 85-94, 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. 278-292, 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. 90-116, Nov. 1990.
[4] R. Balzer, "A 15 year perspective on automatic programming,"IEEE Trans. Software Eng., vol. SE-11, no. 11, pp. 1257-1268, Nov. 1985.
[5] M. Ben-Ari, 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. 361-372, Oct. 1978.
[7] G. V. Bochmann, "Hardware specification with temporal logic: an example,"IEEE Trans. Computers, vol. C-31, pp. 223-231, Mar. 1982.
[8] D. Brand and P. Zafiropulo, "On communicating finite state machines,"J. ACM, vol. 30, no. 2, pp. 323-342, Apr. 1983.
[9] R. J. A. Buhr,System Design with Ada. Englewood Cliffs, NJ: Prentice-Hall, 1984.
[10] R. J. A. Buhr,Practical Visual Techniques for System Design. Englewood Cliffs, NJ: Prentice-Hall, 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. 235-249, Mar. 1989.
[12] R. J. A. Buhret al., "Time Bench: a CAD tool for real-time system design," Dept. Syst. and Comput. Eng., Carleton University, Ottawa, ON, Can., Tech. Rep. SCE-90-17, 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: Springer-Verlag, 1984, pp. 113-127.
[14] 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.
[15] W. F. Clocksin and C. S. Mellish,Programming in Prolog. New York: Springer-Verlag, 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: Addison-Wesley, 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. SE-12, no. 2, pp. 293-311, Feb. 1986.
[19] F. C. Furtek, "Specification and verification of real-time, distributed systems using the theory of constraints," inProc. 5th Int. Conf. on Automated Deduction(Lecture Notes in Computer Science no. 87). New York: Springer-Verlag, 1980, pp. 110-125.
[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. 154-182, Jan. 1986.
[21] B. T. Hailpern,Verifying Concurrent Processes Using Temporal Logic(Lecture Notes in Computer Science no. 129). New York: Springer-Verlag, 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. 331-353, Sept. 1983.
[23] D. Helmbold and D. Luckham, "Debugging Ada tasking programs,"IEEE Software, vol. 2, pp. 47-57, Mar. 1985.
[24] R. C. Holt, E. D. Lazowska, G. Scranaham, and M. A. Scott,Structured Concurrent Design with Operating System Applications. Reading, MA: Addison-Wesley, 1978.
[25] G. M. Karam, "A tool-set 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. SCE-87-2, 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. 36-44.
[27] G. M. Karam and R. J. A. Buhr, "Starvation and critical race analyzers for Ada,"IEEE Trans. Software Eng., vol. 16, pp. 829-843, Aug. 1990.
[28] R. Kowalski,Logic for Problem Solving. New York: North-Holland, 1979.
[29] D. C. Luckham and F. W. Von Henke, "An overview of ANNA: a specification language for Ada,"IEEE Software, vol. 2, pp. 9-23, 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. 215-273.
[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: Springer-Verlag, 1981, pp. 200-252.
[32] R. Milner,A Calculus of Communicating Systems (Lecture Notes in Computer Science 92). New York: Springer-Verlag, 1980.
[33] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE-7, pp. 417-426, 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. 121-131.
[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. 455-495.
[36] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223-252, Sept. 1977.
[37] A. Pnueli and W. P. DeRoever, "Rendezvous with Ada--a proof theoretic view," inProc. AdaTEC Conf. on Ada(Arlington, VA), Oct. 1982, pp. 129-137.
[38] N. Rescher and A. Urquhart,Temporal Logic. New York: Springer-Verlag, 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. Melliar-Smith, "Temporal logic specifications of distributed systems," inProc. 2nd Int. Conf. on Distributed Syst. (Paris), Apr. 1981, pp. 446-454.
[42] R. L. Schwartz and P. M. Melliar-Smith, "From state machines to temporal logic: specification methods for protocol standards,"IEEE Trans. Commun., vol. COM-30, pp. 2486-2496, Dec. 1982.
[43] R. N. Taylor, "A general purpose algorithm for analyzing concurrent programs,"Commun. ACM, vol. 26, no. 5, pp. 362-376, May 1983.
[44] Reference Manual for the Ada Programming Language, U.S. Dept. Defense, Washington, DC, MIL-STD-1815a, 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. SE-12, no. 2, pp. 312-325, Feb. 1986.

Index Terms:
temporal logic-based specification language; deadlock analyzer; Timebench; concurrent system-design environment; specification language; COL; linear-time temporal logic; formal basis; axiomatic reasoning; deadlock analysis tool; reasoning power; Ada designs; systemwide deadlock-free; theorem prover; deadlock algorithm; finite systems; worst-case 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
Citation:
G.M. Karam, R.J.A. Buhr, "Temporal Logic-Based Deadlock Analysis for Ada," IEEE Transactions on Software Engineering, vol. 17, no. 10, pp. 1109-1125, Oct. 1991, doi:10.1109/32.99197
Usage of this product signifies your acceptance of the Terms of Use.