Towards Modelling and Verification of Concurrent Ada Programs Using Petri-Nets
A. Burns, A. J. Wellings, F. Burns, A.M. Koelmans, M. Koutny, A. Romanovsky and A. Yakovlev
Ada 95 is an expressive concurrent programming language with which it is possible to build complex multi-tasking applications. Much of the complexity of these applications stems from the interactions between the tasks. This paper argues that Petri nets offer a promising, tool-supported, technique for checking the logical correctness of the tasking algorithms. The paper illustrates the effectiveness of this approach by showing the correctness of an Ada implementation of the atomic action protocol using a variety of Petri net tools, including PED, PEP and INA for P/T nets and Design/CPN for Coloured Petri nets.
Download Not Available
BibTex Entry
@inproceedings{Burns2000d,
author = {A. Burns and A. J. Wellings and F. Burns and A.M. Koelmans and M. Koutny and A. Romanovsky and A. Yakovlev},
booktitle = {Proc. Workshop Software Engineering and Petri Nets, 21st Int. Conf. App. Theory of Petri Nets, Aarhus, Denmark},
category = {design,languages},
pages = {115--134},
title = {Towards Modelling and Verification of Concurrent Ada Programs Using Petri-Nets},
year = {2000}
}