University of Minnesota
Software Engineering Center
/

You are here

The Hidden Models of Model Checking

Date of Publication: 
October 2012
Associated Research Groups: 
Publication Files: 
Abstract: 
In the past, applying formal analysis, such as model checking, to industrial problems required a team of formal methods experts and a great deal of effort. Model checking has become popular, because model checkers have evolved to allow domain-experts, who lack model checking expertise, to analyze their systems. What made this shift possible and what roles did models play in this? That is the main question we consider here. We survey approaches that transform domain-specific input models into alternative forms that are invisible to the user and which are amenable to model checking using existing techniques—we refer to these as hidden models. We observe that keeping these models hidden from the user is in fact paramount to the success of the domain-specific model checker. We illustrate the value of hidden models by surveying successful examples of their use in different areas of model checking (hardware and software) and how a lack of suitable models hamper a new area (biological systems).
Publisher: 
Springer
Venue: 
Software & Systems Modeling, October 2012, Volume 11, Issue 4, pp 541-555
bibtex: 
@article{Visser2012:hidden-models, year={2012}, issn={1619-1366}, journal={Software & Systems Modeling}, volume={11}, issue={4}, doi={10.1007/s10270-012-0281-9}, title={The hidden models of model checking}, url={http://dx.doi.org/10.1007/s10270-012-0281-9}, publisher={Springer-Verlag}, keywords={Model checking; Models temporal logic; Biological systems}, author={Visser, Willem and Dwyer, MatthewB. and Whalen, Michael}, pages={541-555}, language={English} }