Modelling and verification of an atomic action protocol implemented in Ada

A Burns; A J Wellings; F Burns; A M Koelmans; M Koutny; A Romanovsky; A Yakovlev

Modelling and verification of an atomic action protocol implemented in Ada

A Burns, A J Wellings, F Burns, A M Koelmans, M Koutny, A Romanovsky, A Yakovlev

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 FED, PEP and INA for P/T nets and Design/CPN for Coloured Petri nets.

Original language	English
Pages (from-to)	173-182
Number of pages	10
Journal	Computer systems science and engineering
Volume	16
Issue number	3
Publication status	Published - May 2001

Keywords

Ada 95
atomic action protocol
Petri nets
CHECKING
ALGEBRA

Cite this

@article{9260aefd5c6d409a97969cdc0b966ef8,

title = "Modelling and verification of an atomic action protocol implemented in Ada",

abstract = "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 FED, PEP and INA for P/T nets and Design/CPN for Coloured Petri nets.",

keywords = "Ada 95, atomic action protocol, Petri nets, CHECKING, ALGEBRA",

author = "A Burns and Wellings, {A J} and F Burns and Koelmans, {A M} and M Koutny and A Romanovsky and A Yakovlev",

year = "2001",

month = may,

language = "English",

volume = "16",

pages = "173--182",

journal = "Computer systems science and engineering",

issn = "0267-6192",

publisher = "Tech Science Press",

number = "3",

}

TY - JOUR

T1 - Modelling and verification of an atomic action protocol implemented in Ada

AU - Burns, A

AU - Wellings, A J

AU - Burns, F

AU - Koelmans, A M

AU - Koutny, M

AU - Romanovsky, A

AU - Yakovlev, A

PY - 2001/5

Y1 - 2001/5

N2 - 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 FED, PEP and INA for P/T nets and Design/CPN for Coloured Petri nets.

AB - 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 FED, PEP and INA for P/T nets and Design/CPN for Coloured Petri nets.

KW - Ada 95

KW - atomic action protocol

KW - Petri nets

KW - CHECKING

KW - ALGEBRA

M3 - Article

SN - 0267-6192

VL - 16

SP - 173

EP - 182

JO - Computer systems science and engineering

JF - Computer systems science and engineering

IS - 3

ER -