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 条
  • [21] Formal verification of communication protocols using quantized Horn clauses
    Balu, Radhakrishnan
    QUANTUM INFORMATION AND COMPUTATION IX, 2016, 9873
  • [22] Verification of communication protocols using abstract interpretation of FIFO queues
    Le Gall, Tristan
    Jeannet, Bertrand
    Jeron, Thierry
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, 2006, 4019 : 204 - 219
  • [23] Verification of Symbolic Distributed Protocols for Networked Embedded Devices
    Augello, Andrea
    D'Antoni, Rosolino
    Gaglio, Salvatore
    Lo Re, Giuseppe
    Martorella, Gloria
    Peri, Daniele
    2020 25TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2020, : 1173 - 1176
  • [24] Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
    Damm, Werner
    Dierks, Henning
    Disch, Stefan
    Hagemann, Willem
    Pigorsch, Florian
    Scholl, Christoph
    Waldmann, Uwe
    Wirtz, Boris
    SCIENCE OF COMPUTER PROGRAMMING, 2012, 77 (10-11) : 1122 - 1150
  • [25] ALGEBRAIC SPECIFICATION AND VERIFICATION OF COMMUNICATION PROTOCOLS
    KOOMEN, CJ
    SCIENCE OF COMPUTER PROGRAMMING, 1985, 5 (01) : 1 - 36
  • [26] A　VERIFICATION　METHOD　FOR　COMMUNICATION　PROTOCOLS　MODELED　AS　COMMUNICATING　EXTENDED　FINITE─STATE　MAC
    Shao Fengjing Sun Xiaorui Liu Zunren Department of Computer Qingdao UniversityQingdao
    青岛大学学报(自然科学版), 1996, (03) : 4 - 13
  • [27] A SPECIFICATION AND VERIFICATION TOOL FOR COMMUNICATION PROTOCOLS
    KAUR, H
    GRIER, JB
    CAMPBELL, G
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 507 : 234 - 241
  • [28] Modeling and verification of some communication protocols
    Talukder, KH
    Harada, K
    8th International Conference on Advanced Communication Technology, Vols 1-3: TOWARD THE ERA OF UBIQUITOUS NETWORKS AND SOCIETIES, 2006, : U2193 - U2198
  • [29] Verification of infinite state systems
    Bouajjani, A
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2003, 2803 : 71 - 71
  • [30] COMPOSITIONAL DESIGN AND VERIFICATION OF COMMUNICATION PROTOCOLS, USING LABELED PETRI NETS
    LLORET, JC
    AZEMA, P
    VERNADAT, F
    LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 96 - 105
12345