Composite Model Checking with Type Specific Symbolic Encodings

Abstract

We 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)