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 条
  • [41] From Explicit to Symbolic Types for Communication Protocols in CCS
    Nielson, Hanne Riis
    Nielson, Flemming
    Kreiker, Joerg
    Pilegaard, Henrik
    FORMAL MODELING: ACTORS, OPEN SYSTEMS, BIOLOGICAL SYSTEMS: ESSAYS DEDICATED TO CAROLYN TALCOTT ON THE OCCASION OF HER 70TH BIRTHDAY, 2011, 7000 : 74 - 89
  • [42] MECHANICAL VERIFICATION AND AUTOMATIC IMPLEMENTATION OF COMMUNICATION PROTOCOLS
    BLUMER, TP
    SIDHU, DP
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1986, 12 (08) : 827 - 843
  • [43] FORMAL SPECIFICATION AND VERIFICATION OF SECURE COMMUNICATION PROTOCOLS
    KNAPSKOG, SJ
    LECTURE NOTES IN COMPUTER SCIENCE, 1990, 453 : 58 - 73
  • [44] MODULAR VERIFICATION OF COMPUTER-COMMUNICATION PROTOCOLS
    HAILPERN, BT
    OWICKI, SS
    IEEE TRANSACTIONS ON COMMUNICATIONS, 1983, 31 (01) : 56 - 68
  • [45] Automated Modular Verification for Relaxed Communication Protocols
    Costea, Andreea
    Chin, Wei-Ngan
    Qin, Shengchao
    Craciun, Florin
    PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2018, 2018, 11275 : 284 - 305
  • [46] Foundations of Infinite-State Verification
    Majumdar, Rupak
    SOFTWARE SYSTEMS SAFETY, 2014, 36 : 191 - 222
  • [47] Compositional verification of infinite state systems
    Delzanno, G
    Gabbrielli, M
    Meo, MC
    LOGIC PROGRAMMING, PROCEEDINGS, 2003, 2916 : 47 - 48
  • [48] Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach
    Kobeissi, Nadim
    Bhargavan, Karthikeyan
    Blanchet, Bruno
    Proceedings - 2nd IEEE European Symposium on Security and Privacy, EuroS and P 2017, 2017, : 435 - 450
  • [49] Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach
    Kobeissi, Nadim
    Bhargavan, Karthikeyan
    Blanchet, Bruno
    2017 IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY (EUROS&P), 2017, : 435 - 450
  • [50] Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols
    Blanchet, Bruno
    2017 IEEE 30TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2017, : 68 - 82
12345