Report ID
1999-02
Report Authors
Tevfik Bultan, Richard Gerber, and Christopher League
Report Date
Abstract
In recent years, there has been a surge of progress in automated verificationmethods based on state exploration. In areas like hardware design, thesetechnologies are rapidly augmenting key phases of testing and validation. Todate, one of the most successful of these methods has been symbolic modelchecking, in which large finite-state machines are encoded into compact datastructures such as binary decision diagrams (BDDs) -- and are then checked forsafety and liveness properties.However, these techniques have not realized the same success on softwaresystems. One limitation is their inability to deal with infinite-state programs-- even those with a single unbounded integer. A second problem is that offinding efficient representations for various variable types. We recentlyproposed a model checker for integer-based systems that uses arithmeticconstraints as the underlying state representation. While this approach easilyverified some subtle, infinite-state concurrency problems, it provedinefficient in its treatment of boolean and (unordered) enumerated types --which are not efficiently representable using arithmetic constraints.In this paper we present a new technique that combines the strengths of bothBDD and arithmetic constraint representations. Our composite model mergesmultiple type-specific symbolic representations in a single model checker. Asystem\'s transitions and fixpoint computations are encoded using both BDD (forboolean and enumerated types), and arithmetic constraint (for integers)representations, where the choice depends on the variable types. Our compositemodel checking strategy can be extended to other symbolic representationsprovided that they support operations such as intersection, union, complement,equivalence checking and relational image computations. We also presentconservative approximation techniques for composite representations to addressthe undecidability of model checking on infinite-state systems.We demonstrate the effectiveness of our approach by analyzing two examplesystems which include a mixture of booleans, integers and enumerated types. Oneof them is a requirements specification for the control software of a nuclearreactor\'s cooling system, and the other one is a transport protocolspecification.
Document
1999-02.ps441.23 KB