- The verification and validation research vision is to optimize
explicit state model checking to find and interpret errors in real
world design while retaining [the ability to achieve] exhaustive
coverage. Explicit state model checking is a formal method that
proves a design satisfies, or is a model of, a set of
specifications. Although powerful, this technique is not always
practical in industrial design due to an explosion in the search
space that must be exhaustively explored to complete the
correctness proof. Optimized error discovery
and interpretation may move explicit state model checking closer
to real world application.
- The research methodology in the verification and validation lab
couples theory with empirical analysis. Model checking, [by]
nature, is a mathematically rigorous method with solid
theoretical underpinnings. Our goal in the lab is to leverage the
existing theory and create new theory only when necessary.
Although there is a significant theoretical component to our work,
theory for the sake of theory can become irrelevant. As such, the
lab has focus on improved empirical analysis of new and existing
explicit state model checking algorithms through benchmarking.
The lab is building a freely available database of model checking
problems for identifying areas of strength and weakness in
existing model checking tools. The theoretical emphasis combined
with empirical analysis enables the lab to explore the frontier of
model checking research while remaining relevant.
|
