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 条

[1] Symbolic verification of communication protocols with infinite state spaces using QDDs
Boigelot, B
Godefroid, P
FORMAL METHODS IN SYSTEM DESIGN, 1999, 14 (03) : 237 - 255
[2] Symbolic verification of communication protocols with infinite state spaces using QDDs
Université de Liège, Institut Montefiore, B28, 4000 Liège Sart-Tilman, Belgium
不详
Formal Methods Syst Des, 3 (237-255):
[3] VERIFICATION OF PROTOCOLS USING SYMBOLIC EXECUTION
BRAND, D
JOYNER, WH
COMPUTER NETWORKS AND ISDN SYSTEMS, 1978, 2 (4-5): : 351 - 360
[4] Formal verification of complex coherence protocols using symbolic state models
Hewlett Packard Lab, Palo Alto, United States
J ACM, 4 (557-587):
[5] Formal verification of complex coherence protocols using symbolic state models
Pong, F
Dubois, M
JOURNAL OF THE ACM, 1998, 45 (04) : 557 - 587
[6] VERIFICATION OF THE TRIANGULAR COMMUNICATION GRIDS PROTOCOLS BY INFINITE PETRI NETS
Shmeleva, T. R.
RADIO ELECTRONICS COMPUTER SCIENCE CONTROL, 2018, (04) : 31 - 41
[7] SPECIFICATION AND VERIFICATION OF COMMUNICATION PROTOCOLS IN AFFIRM USING STATE TRANSITION MODELS
SUNSHINE, CA
THOMPSON, DH
ERICKSON, RW
GERHART, SL
SCHWABE, D
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1982, 8 (05) : 460 - 489
[8] VERIFICATION OF SQUARE COMMUNICATION GRID PROTOCOLS VIA INFINITE PETRI NETS
Shmeleva, T. R.
Zaitsev, D. A.
Zaitsev, I. D.
MESM 2009: 10TH MIDDLE EASTERN SIMULATION MULTICONFERENCE, 2009, : 53 - 59
[9] Ensuring completeness of symbolic verification methods for infinite-state systems
Abdulla, PA
Jonsson, B
THEORETICAL COMPUTER SCIENCE, 2001, 256 (1-2) : 145 - 167
[10] Symbolic verification of infinite systems using a finite union of DFAs
Roy, S
PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, 2004, : 56 - 66

← 1 2 3 4 5 →