The increasing complexity of industrial hardware systems has brought into prominence the role of formal verification in the debugging and validation of their designs. While simulation based testing still has great value, the advantages and complementarity of formal verification are now beyond question. Automated verification techniques, especially, have proven to be highly effective. Verification techniques explore the entire state space of a design model and can often find elusive bugs that lurk in the corners of complex designs.; However, verification techniques suffer from the well-known state explosion problem. The large state spaces of complex designs continue to outgrow the capacity of verification techniques. Considerable progress has been made in recent years to enhance the capacities of automated verification tools, including the advent of binary decision diagram (BDD) and satisfiability solver (SAT) based symbolic techniques. Unfortunately, most of these techniques are driven by, and suited to, hardware verification. Many other classes of designs, such as communication protocols from different domains, and software systems, are not easily amenable to either description, or verification, or both, using these symbolic techniques.; This dissertation presents a set of techniques for increasing the power and reach of explicit state-enumeration verification tools for rule based systems, a convenient paradigm for protocol. The techniques have been implemented as extensions to the Murphi verifier, and have been tested on high-level protocol designs of varying sizes, with very promising results. First, we develop an efficient algorithm to perform partial order reduction, a powerful state space reduction technique, on rule-based systems. We then develop techniques to exploit common features of rule-based systems, such as parametricity, symmetry and the transactional nature of many designs, to achieve further state space reduction. Put together, these techniques have resulted in up to a 90% state space reduction.; Another contribution is the design of a translator from the rule-based language of Murphi into the input language of the symbolic model checking tool NuSMV. Based on symbolic simulation, this translator makes state-of-the-art symbolic techniques available to systems modeled in the high-level Murphi language.; As a result of these advancements, many complex systems can now be verified faster, and with much less memory.
展开▼
