符号执行和模型检查(例如在模型转换中)有什么区别?我不明白他们的区别。他们是一样的吗?!符号执行和模型检查
2
A
回答
2
在模型检查中,您必须将您的系统编码为有限状态机,并将该FSM提供给模型检查器以及规范。模型检查器将确保规范始终在该系统中。
在符号执行中,您只提供程序,符号执行引擎将检查所有可行路径以生成测试输入或检查断言。
一个简单的例子:并发性。模型检查可以处理多线程系统,因为它在作为输入提供的FSM中指定,但符号执行不能处理多个线程。
2
模型检查: 正式验证程序是否满足规范的方法。规范通常以一个时态逻辑公式给出,如:“如果输入是x输出必须是y - 对于程序的所有执行(全局)”(例如参见Edward A Lee)。
符号模型检查与显式状态检查: 程序可以是有限状态机(FSM)。这里明确的状态检查就足够了。但幸运的是,模型检查器也适用于扩展的FSM,并发,概率,实时应用程序。为了帮助防止具有非常大(无限)状态的系统中的状态爆炸,使用符号模型检查。 在符号模型中检查状态和输入等被视为符号和命题公式(或状态集合,集合操作等)。为了执行模型检查,需要进行可达性分析,并执行此操作,程序转换将以符号方式执行。这些检查程序不能使用工具化本机代码的正常执行。
符号执行: 在符号执行过程中存在不同的编码方法。有些模型检查非常具体,有些模块是模块化的,并且在象征执行的发明人所定义的独立符号执行框架中使用。一个象征性的执行框架也经常使用符号模型检验的某些元素(勘探,搜索),以用于测试等是可用的
最后一些例子:
JPF,Java的探路者:模型检查,明确检查状态,输入:Java字节码
SPF,符号探路者:符号执行,JPF
JCBMC的延伸:界的模型检查器,JPF的扩展,SPF
XRTs:探索与符号IC执行,输入:CIL字节码
IntelliTest:参数化单元测试使用XRTs
规格资源管理器:基于模型的测试使用XRTs
相关问题
- 1. Scala:执行泛型类型检查
- 2. 在进行注册模块时应执行检查类型
- 3. AC_CHECK_LIB检查什么类型的符号?
- 4. Rails:将模型添加到模型以基于current_user执行检查?
- 5. Django模型继承和类型检查
- 6. 检查模板类型并执行相应的计算
- 7. 在Django的管理员中保存模型时执行检查
- 8. 如何在对模型执行操作之前对相关模型执行复杂的验证检查?
- 9. 静态分析和符号执行中的错误检测
- 10. 可达性和符号执行
- 11. 执行由M文件Simulink模型和检索结果
- 12. 当执行模型
- 13. 执行查找和替换时维护$(美元符号)
- 14. 执行有符号和无符号整数的区别C++
- 15. 模型检查Paxos
- 16. 检查content_object是某型号
- 17. 执行字符串和检索结果
- 18. 模板类型检查参数C++,不同类型的执行路径
- 19. 轨道模型行动检查
- 20. 使用SPIN进行LTL模型检查
- 21. 使用NuSMV进行模型检查
- 22. Django的 - 检查模型有孩子(相关型号)
- 23. 执行带参数模型和查询的queryExecuteFactory时出错
- 24. 检查号码模1
- 25. Pycurl执行()方法,writefunc执行模型
- 26. 解耦模型和输入检查
- 27. 干工程符号执行
- 28. 检查表情符号
- 29. C++对象模型和多态:运行时检查
- 30. 使用Spin和Promela语法进行LTL模型检查
感谢你的帮助。 Java Path Finder是模型检查工具还是符号执行工具或两者? 是否有任何不使用模型检查的符号执行工具? – any