Verifying Programs with Unreliable Channels
Information and ComputationPublished 1 June 1996
Parosh Aziz Abdulla, Bengt Jönsson
Citations354
SJR quartileQ2
SJR score0.49
SNIP0.88
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
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) thereachability problem—is a finite set of global states reachable from some other global state of the system ? (2)safety properties over tracesformulated 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 unboundedperfectFIFO channels.
Keywords
Computer Science
Information and ComputationSymbolic model checking: 1020 States and beyond
2,674 Citations1992Jerry R. Burch, E. M. Clarke +3 more
It is shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata.
Open Repository and Bibliography (University of Liège)An Automata-Theoretic Approach to Automatic Program Verification
1,254 Citations1986Moshe Y. Vardi, Pierre Wolper
Journal of the ACMOn Communicating Finite-State Machines
1,067 Citations1983Daniël Brand, P. Zafiropulo
A model of commumcations protocols based on finite-state machines is investigated and it is determined to what extent the problem is solvable, and one approach to solving it is described.
Journal of Computer and System SciencesParallel program schemata
984 Citations1969Richard M. Karp, Raymond E. Miller
This paper introduces a model called the parallel program schema for the representation and study of programs containing parallel sequencing, related to Ianov's program schema, but extends it, both by modelling memory structure in more detail and by admitting parallel computation.
Model-checking for real-time systems
890 Citations2002Rajeev Alur, Costas Courcoubetis +1 more
An algorithm is developed for model checking, that is, for determining the truth of a TCTL formula with respect to a timed graph, and it is argued that choosing a dense domain, instead of a discrete domain, to model time does not blow up the complexity of the model-checking problem.
Journal of the ACMReasoning about systems with many processes
443 Citations1992Steven M. German, A. Prasad Sistla
Methods are given for automatically verifying temporal properties of concurrent systems containing an arbitrary number of finite-state processes that communicate using CCS actions and how these decision procedures can be used to reason about certain systems with a communication network.
Communications of the ACMA note on reliable full-duplex transmission over half-duplex links
442 Citations1969Keith A. Bartlett, R.A. Scantlebury +1 more
A simple procedure for achieving reliable full-duplex transmission over half-duple links is proposed and is compared with another of the same type, which has recently been described in the literature.
Automatic verification of finite state concurrent system using temporal logic specifications
412 Citations1983E. M. Clarke, E. Allen Emerson +1 more
It is argued that this technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite state concurrent systems.
Formal Methods in System DesignUsing partial orders for the efficient verification of deadlock freedom and safety properties
301 Citations1993Patrice Godefroid, Pierre Wolper
This article presents an algorithm for detecting deadlocks in concurrent finite-state systems without incurring most of the state explosion due to the modeling of concurrency by interleaving that can be much more efficient than the classical exploration of the whole state space.
Computer Networks (1976)Finite state description of communication protocols
282 Citations1978Gregor von Bochmann
The paper discusses different aspects of protocol validation, some verification tools based on the finite state formalism, and the basic limitations of the finitestate modelling of protocols.
ACM Transactions on Programming Languages and SystemsData flow analysis of communicating finite state machines
70 Citations1991Wuxu Peng, S. Puroshothaman
The central technical contribution of this paper is an algorithm to compute approximations to solutions for the ensuing equations that can be used to check that interactions between the processes are free of nonprogress errors.
Lecture notes in computer scienceNetwork grammars, communication behaviors and automatic verification
62 Citations1990Ze'ev Shtadler, Orna Grümberg
Computing and Informatics / Computers and Artificial IntelligenceOn deadlock detection in systems of communicating finite state machines
48 Citations1987Mohamed G. Gouda, Eitan M. Gurari +2 more
Dans le systeme de machines a etats finis considere, les communications se font exclusivement par echange de messages sur des canaux FIFO a voie unique.
Theoretical Computer ScienceBoundedness, empty channel detection, and synchronization for communicating finite automata
26 Citations1986Louis E. Rosier, Hsu‐Chun Yen
In this paper, it is shown that the boundedness problem is decidable for the class of FIFO networks consisting of two such CFSM's, where one of the two machines is allowed to send only a single type of message to the other.
Lecture notes in computer scienceAutomatic temporal verification of buffer systems
16 Citations1992A. Prasad Sistla, Lenore D. Zuck
A formal model for processes that communicate through fifo message buffers is presented and a sound automatic proof system for verifying RTL definable properties of such systems is given and can be applied to some practical examples.