University of Minnesota
Software Engineering Center
/

You are here

Deviation Analysis: A New Use for Model Checking

Date of Publication: 
March 2005
Associated Research Groups: 
Abstract: 
Inaccuracies, or deviations, in the measurements of monitored variables in a control system are facts of life that control software must accommodate. Deviation analysis can be used to determine how a software specification will behave in the face of such deviations. Deviation analysis is intended to answer questions such as "What is the effect on output O if input I is off by 0 to 100?". This property is best checked with some form of symbolic execution approach. In this report we wish to propose a new approach to deviation analysis using model checking techniques. The key observation that allows us to use model checkers is that the property can be restated as "Will there be an effect on output O if input I is off by 0 to 100?"--this restatement of the property changes the analysis from an exploratory analysis to a verification task suitable for model checking.
Publisher: 
Kluwer Academic Publishers
Venue: 
Journal of Automated Software Engineering, volume 12, issue 3
bibtex: 
@article{Heimdahl05:deviation, author = {Heimdahl, Mats P. and Choi, Yunja and Whalen, Michael W.}, title = {Deviation Analysis: A New Use of Model Checking}, journal = {Automated Software Engineering.}, volume = {12}, number = {3}, year = {2005}, issn = {0928-8910}, pages = {321--347}, doi = {http://dx.doi.org/10.1007/s10515-005-2642-x}, publisher = {Kluwer Academic Publishers}, address = {Hingham, MA, USA}, }