符号执行和模型检查

符号执行和模型检查（例如在模型转换中）有什么区别？我不明白他们的区别。他们是一样的吗？！符号执行和模型检查

来源

2016-08-23 any

在模型检查中，您必须将您的系统编码为有限状态机，并将该FSM提供给模型检查器以及规范。模型检查器将确保规范始终在该系统中。

在符号执行中，您只提供程序，符号执行引擎将检查所有可行路径以生成测试输入或检查断言。

一个简单的例子：并发性。模型检查可以处理多线程系统，因为它在作为输入提供的FSM中指定，但符号执行不能处理多个线程。

来源

2016-09-06 20:43:40 afsafzal

感谢你的帮助。 Java Path Finder是模型检查工具还是符号执行工具或两者？是否有任何不使用模型检查的符号执行工具？ – any

模型检查：正式验证程序是否满足规范的方法。规范通常以一个时态逻辑公式给出，如：“如果输入是x输出必须是y - 对于程序的所有执行（全局）”（例如参见Edward A Lee）。

符号模型检查与显式状态检查：程序可以是有限状态机（FSM）。这里明确的状态检查就足够了。但幸运的是，模型检查器也适用于扩展的FSM，并发，概率，实时应用程序。为了帮助防止具有非常大（无限）状态的系统中的状态爆炸，使用符号模型检查。在符号模型中检查状态和输入等被视为符号和命题公式（或状态集合，集合操作等）。为了执行模型检查，需要进行可达性分析，并执行此操作，程序转换将以符号方式执行。这些检查程序不能使用工具化本机代码的正常执行。

符号执行：在符号执行过程中存在不同的编码方法。有些模型检查非常具体，有些模块是模块化的，并且在象征执行的发明人所定义的独立符号执行框架中使用。一个象征性的执行框架也经常使用符号模型检验的某些元素（勘探，搜索），以用于测试等是可用的

最后一些例子：

JPF，Java的探路者：模型检查，明确检查状态，输入：Java字节码

SPF，符号探路者：符号执行，JPF

JCBMC的延伸：界的模型检查器，JPF的扩展，SPF

XRTs：探索与符号IC执行，输入：CIL字节码

IntelliTest：参数化单元测试使用XRTs

规格资源管理器：基于模型的测试使用XRTs

来源

2017-04-15 13:33:51 goofy

符号执行和模型检查

回答

相关问题