Verifying Programs with Unreliable Channels

We consider the veri cation of a particular class of in nite-state systems, namely systems consisting of nite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model e.g. link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, we show that several interesting veri cation problems are decidable by giving algorithms for verifying (1) the reachability problem: is a nite set of global states reachable from some other global state of the system, (2) safety properties over traces formulated as regular sets of allowed nite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. We have used the algorithms to verify some idealized sliding-window protocols with reasonable time and space resources. Our results should be contrasted with the well-known fact that these problems are undecidable for systems with unbounded perfect FIFO channels.

• Type: Conference
• Year: 1993
• Where: LICS
• Authors: Parosh Aziz Abdulla, Bengt Jonsson
• Keywords: Automated Reasoning, FIFO Channels, LICS 1993, Unbounded Lossy Fifo, Veri Cation