Compositional Petri net models of advanced tasking in Ada-95

The Ada language has been designed to support development of concurrent and distributed software. While the Ada-83 standard defined the basic mechanis ms of rendezvous-based tasking, the Ada-95 standard significantly extended this capability with the introduction of several advanced tasking construct s. We present and discuss formal models of these key tasking constructs usi ng the Petri net model. We also provide some formal evaluation of the model s using one particular net-based method, invariant analysis. The constructs considered are the asynchronous transfer of control, the protected object, and the requeue statement. By modeling these advanced Ada tasking construc ts with Petri nets, we obtain compositional models of the constructs that a re complementary to earlier work in net-based modeling of Ada tasking, both in terms of de fining precise behavior for tasking semantics, and also in terms of providing support for automated analysis of concurrent software. ( C) 2000 Elsevier Science Ltd. All rights reserved.