FORMAL ANALYSIS OF THE ALTERNATING BIT PROTOCOL BY TEMPORAL PETRI NETS

被引：24

作者：

SUZUKI, I

机构：

[1] Department of Electrical Engineering and Computer Science, University of Wisconsin—Milwaukee, Milwaukee, WI 53201

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1990年 / 16卷 / 11期

关键词：

Alternating bit protocol; Buchi-automaton; formal verification; Petri net; temporal logic; ω-regular expression;

D O I：

10.1109/32.60315

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Temporal Petri nets are Petri nets in which certain restrictions on the firings of transitions are represented by formulas containing temporal operators. We show how temporal Petri nets can be used for formal specification and verification of the alternating bit protocol. The temporal Petri net which models the protocol is analyzed formally by using the existing theory of ^-regular expressions and Buchi-automata. © 1990 IEEE

引用

页码：1273 / 1281

页数：9

共 30 条

[1] VERIFYING TEMPORAL PROPERTIES WITHOUT TEMPORAL LOGIC [J].

ALPERN, B ;

SCHNEIDER, FB .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1989, 11 (01) :147-167

[2] A NOTE ON RELIABLE FULL-DUPLEX TRANSMISSION OVER HALF-DUPLEX LINLS [J].

BARTLETT, KA ;

SCANTLEBURY, RA ;

WILKINSON, PT ;

LYNCH, WC .

COMMUNICATIONS OF THE ACM, 1969, 12 (05) :260-+

[3]

BUCHI JR, 1962, 1960 P INT C LOG MET

[4] THEORIES OF AUTOMATA ON OMEGA-TAPES - SIMPLIFIED APPROACH [J].

CHOUEKA, Y .

JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1974, 8 (02) :117-141

[5] SYSTEM MODELING WITH HIGH-LEVEL PETRI NETS [J].

GENRICH, HJ ;

LAUTENBACH, K .

THEORETICAL COMPUTER SCIENCE, 1981, 13 (01) :109-136

[6] MODULAR VERIFICATION OF COMPUTER-COMMUNICATION PROTOCOLS [J].

HAILPERN, BT ;

OWICKI, SS .

IEEE TRANSACTIONS ON COMMUNICATIONS, 1983, 31 (01) :56-68

[7]

Kleene S.C., 1956, AUTOMATA STUDIES, P3

[8] SPECIFYING CONCURRENT PROGRAM MODULES [J].

LAMPORT, L .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1983, 5 (02) :190-222

[9]

LANDWEBER LH, 1969, MATHEMATICAL SYSTEMS, V3, P376

[10]

LU H, 1987, 29TH P MIDW S CIRC S, P823

← 1 2 3 →