DocumentCode
1336317
Title
Formal analysis of the alternating bit protocol by temporal Petri nets
Author
Suzuki, Ichiro
Author_Institution
Dept. of Electr. Eng. & Comput. Sci., Wisconsin Univ., Milwaukee, WI, USA
Volume
16
Issue
11
fYear
1990
fDate
11/1/1990 12:00:00 AM
Firstpage
1273
Lastpage
1281
Abstract
Temporal Petri nets are Petri nets in which certain restrictions on the firings of transitions are represented by formulas containing temporal operators. The use of temporal Petri nets for formal specification and verification of the alternating bit protocol is discussed. The temporal Petri net which models the protocol is analyzed formally using the existing theory of ω-regular expressions and Buchi-automata
Keywords
Petri nets; automata theory; formal specification; program verification; programming theory; ω-regular expressions; Buchi-automata; alternating bit protocol; firings; formal analysis; formal specification; formal verification; formulas; temporal Petri nets; temporal operators; transitions; Computer simulation; Formal specifications; Logic; Petri nets; Protocols; Safety; Timing; Transmission line theory; Transmission lines;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/32.60315
Filename
60315
Link To Document