On Developing and Verifying Design Abstractions for Reliable Concurrent Programming in Ada

Ada 95 is an expressive concurrent programming lan-guage, which allows building large multi-tasking applica-tions. Much of the complexity of these applications stems from the interactions between the tasks. Design abstrac-tions (such as atomic actions, conversations etc.) have been proposed to deal with such complexity. This paper argues that Petri nets offer a promising, tool-supported, technique for checking the logical correctness of abstractions. The paper illustrates the effectiveness of this approach by show-ing the correctness of an Ada implementation of the atomic action protocol using a variety of Petri net tools. 1