FAST verification of the class of Stop-and-Wait Protocols Modelled by Coloured Petri Nets
Laure Petrucci, Jonathan Billington, Guy Edward Gallasch · HAL (Le Centre pour la Communication Scientifique Directe) · 2005
Most protocols contain parameters, such as the maximum number of retransmissions in an error recovery protocol. These parameters are instantiated with values that depend on the operating environment of the protocol. We would therefore like our formal specification or model of the system to include these parameters symbolically, where in general each parameter will have an arbitrary upper limit. The inclusion of parameters results in an infinite family of finite state systems, which makes verification difficult. However, techniques and tools are being developed for the verification of parametric and infinite state systems. We explore the use of one such tool, FAST, for automatically verifying several properties (such as channel bounds and the stop-and-wait property of alternating sends and receives) of the stop-and-wait class of protocols, where the maximum number of retransmissions and the maximum sequence number are considered as unbounded parameters. Coloured Petri nets (CPNs), an expressive language for representing protocols, is used to model this stop-and-wait class. However, FAST'S foundation is counter systems, automata where states are a vector of non-negative integers and with operations limited to Presburger arithmetic. We therefore also present some first steps in transforming CPNs to counter systems in the context of stop-and-wait protocols operating over unbounded FIFO channels.