Modelling and verification of an atomic action protocol implemented in Ada

Ada 95 is an expressive concurrent programming language with which it is po ssible to build complex multi-tasking applications. Much of the complexity of these applications stems from the interactions between the tasks. This p aper argues that Petri nets offer a promising, tool-supported, technique fo r checking the logical correctness of the tasking algorithms. The paper ill ustrates the effectiveness of this approach by showing the correctness of a n Ada implementation of the atomic action protocol using a variety of Petri net tools, including FED, PEP and INA for P/T nets and Design/CPN for Colo ured Petri nets.