any*_*any 5 validation verification model-driven model-checking
符号执行和模型检查之间有什么区别(例如在模型转换中)？我不明白他们的区别.它们是一样的吗？!
在模型检查中，您必须将系统编码为有限状态机，并向模型检查器提供 FSM 以及规范。然后，模型检查器将确保该规范始终保留在该系统中。
在符号执行中，您只需提供程序，符号执行引擎将检查所有可行路径以生成测试输入或检查断言。
一个简单的例子可以说明它们的区别：并发性。模型检查可以处理多线程系统，因为它是在作为输入提供的 FSM 中指定的，但是符号执行不能处理多个线程。
模型检查：一种正式验证程序是否满足规范的方法。该规范通常以时序逻辑公式给出，例如：“如果输入是x，则输出必须是y - 适用于程序的所有执行（全局）”（参见Edward A Lee）。
符号模型检查与显式状态检查：程序可以是有限状态机 (FSM)。这里显式的状态检查就足够了。但幸运的是，模型检查器也适用于扩展 FSM、并发、概率、实时应用程序。为了帮助防止具有大量（无限）状态的系统中的状态爆炸，使用了符号模型检查。在符号模型检查中，状态和输入等被视为符号和命题公式（或状态集、集合运算等）。为了执行模型检查，需要进行可达性分析，并且为此以符号方式执行程序转换。这些检查器无法利用已检测的本机代码的正常执行。
符号执行：符号执行期间存在不同的编码方法。有些是非常特定于模型检查的，有些是模块化的并在独立的符号执行框架中使用，因为它是由符号执行的发明者定义的。符号执行框架通常还使用符号模型检查的一些元素（探索、搜索）以可用于测试等。
最后一些例子：
JPF，Java-Pathfinder：模型检查器，显式状态检查，输入：java字节码
SPF，Symbolic Pathfinder：符号执行，JPF的扩展
JCBMC：有界模型检查器，JPF、SPF 的扩展
XRT：探索和符号执行，输入：CIL 字节码
IntelliTest：参数化单元测试使用 XRT
Spec Explorer：使用 XRT 进行基于模型的测试
| 归档时间： |
|
| 查看次数： |
830 次 |
| 最近记录： |