Verifying Programs with Unreliable Channels

Abstract

We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-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 verification problems are decidable by giving algorithms for verifying (1) the reachability problem - is a finite set of global states reachable from some other global state of the system? (2) safety properties over traces formulated as regular sets of allowed finite 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. © 1996 Academic Press, Inc.