Composite Model Checking with Type Specific Symbolic Encodings

dc.contributor.authorBultan, Tevfiken_US
dc.contributor.authorGerber, Richarden_US
dc.description.abstractWe present a new symbolic model checking technique, which analyzes temporal properties in multi-typed transition systems. Specifically, the method uses multiple type-specific data encodings to represent system states, and it carries out fixpoint computations via the corresponding type-specific symbolic operations. In essence, different symbolic encodings are unified into one composite model checker. Any type-specific language can be included in this framework -- provided that the language is closed under Boolean connectives, propositions can be checked for satisfiability, and relational images can be computed. Our technique relies on conjunctive partitioning of transition relations of atomic events based on variable types involved, which allows independent computation of one-step pre- and post-conditions for each variable type. In this paper we demonstrate the effectiveness of our method on a nontrivial data-transfer protocol, which contains a mixture of integer and Boolean-valued variables. The protocol operates over an unreliable channel that can lose, duplicate or reorder messages. Moreover, the protocol's send and receive window sizes are not specified in advance; rather, they are represented as symbolic constants. The resulting system was automatically verified using our composite model checking approach, in concert with a conservative approximation technique. (Also cross-referenced as UMIACS-TR-98-07)en_US
dc.format.extent199490 bytes
dc.relation.isAvailableAtDigital Repository at the University of Marylanden_US
dc.relation.isAvailableAtUniversity of Maryland (College Park, Md.)en_US
dc.relation.isAvailableAtTech Reports in Computer Science and Engineeringen_US
dc.relation.isAvailableAtUMIACS Technical Reportsen_US
dc.relation.ispartofseriesUM Computer Science Department; CS-TR-3871en_US
dc.relation.ispartofseriesUMIACS; UMIACS-TR-98-07en_US
dc.titleComposite Model Checking with Type Specific Symbolic Encodingsen_US
dc.typeTechnical Reporten_US


Original bundle
Now showing 1 - 2 of 2
No Thumbnail Available
194.81 KB
Postscript Files
Thumbnail Image
214.77 KB
Adobe Portable Document Format
Auto-generated copy of