In: Microelectronics and Reliability, Vol. 31, No. 4, pages 577-594. 1991.
Abstract: The paper gives a translation of a subset of the programming language Ada to Petri nets. The subset contains Ada rendezvous and dynamic task creation, but does not contain loops. The design of the translation algorithm was influenced by methods of denotational semantics. Properties of a concurrent Ada program can be studied by analyzing the Petri net model. It is possible to determine the possible interleavings of statements and do static deadlock detection. The authors are interested in applying the models of Ada programs to the problem of determining which program segments form the critical path in the time it takes an Ada program to execute.
Keywords: net model (of) concurrent Ada Program; Ada rendezvous (and) dynamic task; denotational semantics; interleaving (of) Ada statements; deadlock detection; critical path.