Petri net models of concurrent Ada programs

A subset of the programming language Ada is translated to Petri nets. The subset contains the Ada rendezvous and dynamic task creation. The design of the translation algorithm was influenced by methods of denotational semantics, which made the implementation of the algorithm particularly simple in the programming language ML. 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 dead-lock detection. The authors investigate applying the models of Ada programs to the problem of determining which program segments form the critical path in the time it takes for execution of an Ada program