As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice.
To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time---a feature suitable for regression verification.
Proceedings of the 18th IEEE International Conference on Automated Software Engineering - Short paper session. Montreal, Canada, October 2003.
Associated research group: Critical Systems Research Group
Choi, Yunja; Heimdahl, Mats.
Model Checking Requirements Specifications Using Domain Reduction Abstraction.
Retrieved from the University of Minnesota Digital Conservancy,
Content distributed via the University of Minnesota's Digital Conservancy may be subject to additional license and use restrictions applied by the depositor.