Colored Petri net models of concurrent Ada programs

A translation is presented of a subset of the programming language Ada to colored Petri nets. The subset contains the Ada rendezvous and dynamic task creation but does not contain loops. The author uses colored nets to cut down the complexity of rendezvous and to include subprocedures and generics. 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