Deviation Analysis: A New Use of Model Checking
Deviation Analysis: A New Use of Model Checking
复制标题
偏差分析：模型检查的新用途
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
M. Whalen
中科院分区：
文献类型：
--
作者：
M. Heimdahl;Yunja Choi;M. Whalen
控制系统中监控变量的测量不准确或偏差是控制软件必须适应的生活事实。偏差分析可以用来确定软件规范在面对这种偏差时会如何表现。偏差分析旨在回答诸如“如果输入I偏离0到100，对输出O有什么影响？”之类的问题。此属性最好使用某种形式的符号执行方法进行检查。在本报告中，我们希望提出一种使用模型检查技术进行偏差分析的新方法。允许我们使用模型检查器的关键观察是，属性可以重新表述为“如果输入I偏离0到100，会对输出O产生影响吗？”——这个属性的重述将分析从探索性分析转变为适合模型检查的验证任务。
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.