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)