Verifying programs with unreliable channels
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 160-170
- https://doi.org/10.1109/lics.1993.287591
Abstract
The verification of a particular class of infinite-state systems, namely, systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels, is considered. This class is able to model, e.g., link protocols such as the Alternating Bit Protocol and HDLC. For this class of systems, it is shown that several interesting verification problems are decidable by giving algorithms for verifying: the reachability problem (whether a finite set of global states is reachable from some other global state of the system); the safety property over traces, formulated as regular sets of allowed finite traces; and eventuality properties (whether all computations of a system eventually reach a given set of states). The algorithms are used to verify some idealized sliding-window protocols with reasonable time and space resources.Keywords
This publication has 11 references indexed in Scilit:
- Model-checking for real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Reasoning about systems with many processesJournal of the ACM, 1992
- Data flow analysis of communicating finite state machinesACM Transactions on Programming Languages and Systems, 1991
- Boundedness, empty channel detection, and synchronization for communicating finite automataTheoretical Computer Science, 1986
- On Communicating Finite-State MachinesJournal of the ACM, 1983
- Automatic verification of finite state concurrent system using temporal logic specificationsPublished by Association for Computing Machinery (ACM) ,1983
- Finite state description of communication protocolsComputer Networks (1976), 1978
- Parallel program schemataJournal of Computer and System Sciences, 1969
- A note on reliable full-duplex transmission over half-duplex linksCommunications of the ACM, 1969
- Ordering by Divisibility in Abstract AlgebrasProceedings of the London Mathematical Society, 1952