University of Minnesota
Software Engineering Center

You are here

Model Checking Requirements Specifications Using Domain Reduction Abstraction

Date of Publication: 
October 2003
Associated Research Groups: 
Publication Files: 
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.