Deviation analysis: A new use of model checking

Research output: Contribution to journalArticlepeer-review

21 Scopus citations

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.

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

Keywords

  • Deviation analysis
  • Model checking
  • Robustness

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

Cite this