Title :
Specification and verification of the alternating bit protocol by temporal Petri nets
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Wisconsin Univ., Milwaukee, WI, USA
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;
Conference_Titel :
Circuits and Systems, 1989., Proceedings of the 32nd Midwest Symposium on
Conference_Location :
Champaign, IL
DOI :
10.1109/MWSCAS.1989.101818
