Composite model-checking: Verification with type-specific symbolic representations

There has been a surge of progress in automated verification methods based on state exploration. In areas like hardware design, these technologies are rapidly augmenting key phases of testing and validation. To date, one of t he most successful of these methods has been symbolic model-checking, in wh ich large finite-state machines are encoded into compact data structures su ch as Binary Decision Diagrams (BDDs), and are then checked for safety and liveness properties. However, these techniques have not realized the same s uccess on software systems. One Limitation is their inability to deal with infinite-state programs, even those with a single unbounded integer. A seco nd problem is that of finding efficient representations for various variabl e types. We recently proposed a model-checker for integer-based systems tha t uses arithmetic constraints as the underlying state representation. While this approach easily verified some subtle, infinite-state concurrency prob lems, it proved inefficient in its treatment of boolean and (unordered) enu merated types-which are not efficiently representable using arithmetic cons traints. In this article we present a new technique that combines the stren gths of both BDD and arithmetic constraint representations. Our composite m odel merges multiple type-specific symbolic representations in a single mod el-checker. A system's transitions and fixpoint computations are encoded us ing both BDD (for boolean and enumerated types) and arithmetic constraint ( for integers) representations, where the choice depends on the variable typ es. Our composite model-checking strategy can be extended to other symbolic representations provided that they support operations such as intersection , union, complement, equivalence checking, and relational image computation . We also present conservative approximation techniques for composite repre sentations to address the undecidability of model-checking on infinite-stat e systems. We demonstrate the effectiveness of our approach by analyzing tw o example software specifications which include a mixture of booleans, inte gers, and enumerated types. One of them is a requirements specification for the control software of a nuclear reactor's cooling system, and the other one is a transport protocol specification.