Title :
Formal analysis of the alternating bit protocol by temporal Petri nets
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Wisconsin Univ., Milwaukee, WI, USA
fDate :
11/1/1990 12:00:00 AM
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;
Journal_Title :
Software Engineering, IEEE Transactions on
