Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs

被引：0
|
作者：
Bernard Boigelot
Patrice Godefroid
机构：
[1] Université de Liège,Institut Montefiore
[2] Lucent Technologies,Bell Laboratories
来源：
Formal Methods in System Design | 1999年 / 14卷
关键词：
symbolic verification; protocols; infinite state spaces; queues; model checking; testing;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
We study the verification of properties of communication protocols modeled by a finite set of finite-state machines that communicate by exchanging messages via unbounded FIFO queues. It is well-known that most interesting verification problems, such as deadlock detection, are undecidable for this class of systems. However, in practice, these verification problems may very well turn out to be decidable for a subclass containing most “real” protocols.
引用
收藏
页码：237 / 255
页数：18
相关论文
共 50 条
  • [31] Symbolic model checking of infinite-state systems using narrowing
    Escobar, Santiago
    Meseguer, Jose
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2007, 4533 : 153 - +
  • [32] Symbolic model checking of infinite state systems using Presburger arithmetic
    Bultan, T
    Gerber, R
    Pugh, W
    COMPUTER AIDED VERIFICATION, 1997, 1254 : 400 - 411
  • [33] Minimization of large state spaces using symbolic branching bisimulation
    Wimmer, Ralf
    Herbstritt, Marc
    Becker, Bernd
    PROCEEDINGS OF THE 2006 IEEE WORKSHOP ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS, 2006, : 8 - +
  • [34] Formal verification of infinite state systems using Boolean methods
    Bryant, Randal E.
    TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2006, 4098 : 1 - 3
  • [35] Verification of sets of infinite state processes using program transformation
    Fioravanti, F
    Pettorossi, A
    Proietti, M
    LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2002, 2372 : 111 - 128
  • [36] Formal verification of infinite state systems using Boolean methods
    Bryant, Randal E.
    21st Annual IEEE Symposium on Logic in Computer Science, Proceedings, 2006, : 3 - 4
  • [37] Symbolic Quick Error Detection Using Symbolic Initial State for Pre-Silicon Verification
    Fadiheh, Mohammad Rahmani
    Urdahl, Joakim
    Nuthakki, Srinivas Shashank
    Mitra, Subhasish
    Barrett, Clark
    Stoffel, Dominik
    Kunz, Wolfgang
    PROCEEDINGS OF THE 2018 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2018, : 55 - 60
  • [38] Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif
    Okazaki, Hiroyuki
    Futa, Yuichi
    Arai, Kenichi
    PROCEEDINGS OF 2018 INTERNATIONAL SYMPOSIUM ON INFORMATION THEORY AND ITS APPLICATIONS (ISITA2018), 2018, : 326 - 330
  • [39] Automatic Verification of Security Protocols in the Symbolic Model: The Verifier Proverif
    Blanchet, Bruno (Bruno.Blanchet@inria.fr), 1600, Springer Verlag (8604):
  • [40] Verification of finite-state-machine refinements using a symbolic methodology
    Hendricx, S
    Claesen, L
    CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 : 326 - 329
12345