DocumentCode :
2721616
Title :
Symbolic protocol verification with queue BDDs
Author :
Godefroid, Patrice ; Long, David E.
fYear :
1996
fDate :
27-30 Jul 1996
Firstpage :
198
Lastpage :
206
Abstract :
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
Keywords :
data structures; decision tables; formal verification; logic testing; protocols; queueing theory; symbol manipulation; Binary Decision Diagrams; Queue BDDs; data types; digital hardware; dynamic data structures; protocol verification; symbolic verification; verification of communication protocols; Automata; Binary decision diagrams; Boolean functions; Data structures; Encoding; Hardware; Protocols; Software systems; Space exploration; State-space methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science, 1996. LICS '96. Proceedings., Eleventh Annual IEEE Symposium on
Conference_Location :
New Brunswick, NJ
ISSN :
1043-6871
Print_ISBN :
0-8186-7463-6
Type :
conf
DOI :
10.1109/LICS.1996.561318
Filename :
561318
Link To Document :
بازگشت