Title :
Model Checking for Protocols Using Verds
Author_Institution :
State Key Lab. of Comput. Sci., Chinese Acad. of Sci., Beijing, China
Abstract :
We present the techniques of ternary boolean diagram-based model checking together with bounded semantics model checking used in the model checker called Verds, which is developed in our laboratory. In the experiment of protocol verification under different scenarios, we compare the performance of Verds against those of model checkers CMurphi and NuSMV, showing that Verds overall compares favorably to NuSMV and CMurphi.
Keywords :
Boolean algebra; formal verification; protocols; ternary logic; Verds model checker; bounded semantics model checking; protocol verification; ternary Boolean diagram-based model checking technique; Boolean functions; Coherence; Computational modeling; Data structures; Memory management; Protocols; Semantics; Verds; model checking; protocol verification;
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2011 Fifth International Symposium on
Conference_Location :
Xi´an, Shaanxi
Print_ISBN :
978-1-4577-1487-0
DOI :
10.1109/TASE.2011.17
