Deviation analysis: A new use of model checking

Research output: Contribution to journalArticlepeer-review

21 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)321-347
Number of pages27
JournalAutomated Software Engineering
Issue number3
StatePublished - Jul 2005

Bibliographical note

Funding Information:
This work has been partially supported by NASA grant NAG-1-224 and NASA contract NCC-01-001. We also want to thank the McKnight Foundation for their generous support over the years.


  • Deviation analysis
  • Model checking
  • Robustness


Dive into the research topics of 'Deviation analysis: A new use of model checking'. Together they form a unique fingerprint.

Cite this