Virtual Collaboration Portal

A deadlock analysis technique based on enumeration of paths (possible interleavings of the execution paths of individual Ada tasks in a concurrent program was described in a previous paper. The work was flawed in many areas, however: the characterization of operational and axiomatic proof methods was muddled and inaccurate, the classification of modeling techniques for concurrent systems confuses the relatively unimportant distinction between state-based and event-based models with the essential distinction between explicit enumeration of behaviors and symbolic manipulation of properties, the statements about the limitations of linear-time temporal logic in relation to nondeterminism are inaccurate, and the characterization of the computational complexity of the analysis technique is overly optimistic. The Ada program used to illustrate the technique was syntactically incorrect.