DocumentCode
1959415
Title
Specification and verification 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
fYear
1989
fDate
14-16 Aug 1989
Firstpage
157
Abstract
Temporal Petri nets are Petri nets in which certain restrictions on the firings of transitions are represented by formulas containing temporal operators. It is shown 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 using the existing theory of ω-regular expressions and Buchi-automata
Keywords
Petri nets; automata theory; multiprocessing systems; protocols; ω-regular expressions; Buchi-automata; alternating bit protocol; firings; formal specification; temporal Petri nets; verification; Fires; Formal specifications; Logic; Petri nets; Process control; Protocols; Safety; Transmission line theory; Transmission lines;
fLanguage
English
Publisher
ieee
Conference_Titel
Circuits and Systems, 1989., Proceedings of the 32nd Midwest Symposium on
Conference_Location
Champaign, IL
Type
conf
DOI
10.1109/MWSCAS.1989.101818
Filename
101818
Link To Document