Logic in Computer Science (LICS 1993)

Paper: Verifying programs with unreliable channels (at LICS 1993)

Authors: Parosh Abdulla Bengt Jonsson

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

BibTeX

  @InProceedings{AbdullaJonsson-Verifyingprogramswi,
    author = 	 {Parosh Abdulla and Bengt Jonsson},
    title = 	 {Verifying programs with unreliable channels},
    booktitle =  {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {160--170},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }