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 language | English (US) |
|---|---|
| Pages (from-to) | 321-347 |
| Number of pages | 27 |
| Journal | Automated Software Engineering |
| Volume | 12 |
| Issue number | 3 |
| DOIs | |
| State | Published - 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.
Keywords
- Deviation analysis
- Model checking
- Robustness