Symbolic Protocol Verification with Queue BDDs

被引：0
|
作者：
Patrice Godefroid
David E. Long
机构：
[1] Lucent Technologies,Bell Laboratories
[2] Lucent Technologies,Bell Laboratories
来源：
Formal Methods in System Design | 1999年 / 14卷
关键词：
communication protocols; queues; symbolic verification; BDDs; state explosion; state-space exploration; model checking;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
Symbolic verification based on Binary Decision Diagrams (BDDs) has proven to be a powerful technique for ensuring the correctness of digital hardware. In contrast, BDDs have not caught on as widely for software verification, partly because the data types used in software are more complicated than those used in hardware. In this work, we propose an extension of BDDs for dealing with dynamic data structures. Specifically, we focus on queues, since they are commonly used in modeling communication protocols. We introduce Queue BDDs (QBDDs), which include all the power of BDDs while also providing an efficient representation of queue contents. Experimental results show that QBDDs are well-suited for the verification of communication protocols.
引用
收藏
页码：257 / 271
页数：14
相关论文
共 50 条
  • [21] DY☆: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code
    Bhargavan, Karthikeyan
    Bichhawat, Abhishek
    Quoc Huy Do
    Hosseyni, Pedram
    Kuesters, Ralf
    Schmitz, Guido
    Wuertele, Tim
    [J]. 2021 IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY (EUROS&P 2021), 2021, : 523 - 542
  • [22] Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol
    Abdulla, P
    Annichini, A
    Bouajjani, A
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1999, 1579 : 208 - 222
  • [23] A SIMPLE THEOREM PROVER BASED ON SYMBOLIC TRAJECTORY EVALUATION AND BDDS
    HAZELHURST, S
    SEGER, CJH
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1995, 14 (04) : 413 - 422
  • [24] Efficient combinational verification using BDDs and a hash table
    Mukherjee, R
    Jain, J
    Takayama, K
    Fujita, M
    Abraham, JA
    Fussell, DS
    [J]. ISCAS '97 - PROCEEDINGS OF 1997 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS, VOLS I - IV: CIRCUITS AND SYSTEMS IN THE INFORMATION AGE, 1997, : 1025 - 1028
  • [25] Rule-based Verification of Network Protocol Implementations using Symbolic Execution
    Song, JaeSeung
    Ma, Tiejun
    Cadar, Cristian
    Pietzuch, Peter
    [J]. 2011 20TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS (ICCCN), 2011,
  • [26] Symbolic language representations for parametric verification of the revised capability exchange signalling protocol
    Liu, Lin
    Billington, Jonathan
    [J]. EIGHTH INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED COMPUTING, APPLICATIONS AND TECHNOLOGIES, PROCEEDINGS, 2007, : 480 - +
  • [27] First-Order Timed Runtime Verification Using BDDs
    Havelund, Klaus
    Peled, Doron
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2020), 2020, 12302 : 3 - 24
  • [28] EXTENDED BDDS - TRADING OFF CANONICITY FOR STRUCTURE IN VERIFICATION ALGORITHMS
    PLESSIER, B
    HACHTEL, G
    SOMENZI, F
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 1994, 4 (02) : 167 - 185
  • [29] BOOLEAN MANIPULATION WITH FREE BDDS - AN APPLICATION IN COMBINATIONAL LOGIC VERIFICATION
    GERGOV, J
    MEINEL, C
    [J]. INFORMATION PROCESSING '94, VOL I: TECHNOLOGY AND FOUNDATIONS, 1994, 51 : 309 - 314
  • [30] HARDWARE-VERIFICATION USING FIRST-ORDER BDDS
    SCHNEIDER, K
    KUMAR, R
    KROPF, T
    [J]. COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 45 - 62
12345