Issue No. 08 - August (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.57622
<p>Starvation and critical race analysis tools for Ada designs are described. These tools are part of a temporal analysis toolset that includes an operational specification language, a language interpreter, and a deadlock analyzer for Ada. The starvation analyzer is based on a set-theoretic model of starvation. It uses a proof tree produced by the deadlock analyzer to define the possible computation space of the design. A preprocessing phase of the starvation tool optimizes the analysis so that the resulting analysis is efficient. Unlike livelock analysis in state machines, the starvation analyzer does not require a priori specification of home states to discern liveness. The critical race analysis tool provides semiautomatic proof of critical races by identifying nondeterministic rendezvous (races) from the proof tree generated by the deadlock analyzer, and then assisting the human operator in identifying which of these constitute critical races. Several design examples are used to demonstrate the capabilities of the two analysis methods.</p>
race analyzers; critical race analysis tools; Ada designs; temporal analysis toolset; operational specification language; language interpreter; deadlock analyzer; starvation analyzer; set-theoretic model; deadlock analyzer; computation space; preprocessing phase; starvation tool; liveness; semiautomatic proof; nondeterministic rendezvous; human operator; design examples; Ada; program interpreters; programming; software tools; specification languages; system recovery.
R. Buhr and G. Karam, "Starvation and Critical Race Analyzers for Ada," in IEEE Transactions on Software Engineering, vol. 16, no. , pp. 829-843, 1990.