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