The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.10 - October (1991 vol.17)
pp: 1109-1125
ABSTRACT
<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>
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, October 1991, doi:10.1109/32.99197
22 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool