Record:   Prev Next
Author Bhattacharya, Ritwik
Title Efficient protocol verification using rule-based systems
book jacket
Descript 102 p
Note Source: Dissertation Abstracts International, Volume: 67-03, Section: B, page: 1509
Adviser: Ganesh Gopalakrishnan
Thesis (Ph.D.)--The University of Utah, 2006
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
School code: 0240
Host Item Dissertation Abstracts International 67-03B
Subject Computer Science
Alt Author The University of Utah
Record:   Prev Next