Issue No. 10 - October (1991 vol. 17)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.99197
<p>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 .</p>
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
G. Karam and R. Buhr, "Temporal Logic-Based Deadlock Analysis for Ada," in IEEE Transactions on Software Engineering, vol. 17, no. , pp. 1109-1125, 1991.