最近，我开始研究形式化验证技术。在文献中，模型检查器和求解器以某种方式互换使用。但是，模型检查器和求解器如何相互连接？
ps 如果建议一些论文或链接，我将不胜感激。
问问题
1342 次
2 回答
5
在模型检查中，您有一个模型和一个规范（或属性），并检查模型是否符合规范。
在 SAT 解题中，你有一个公式，然后你试图找到一个令人满意的作业。
现在，在模型检查中，您可以结合模型和属性的否定来给您一个公式。使用求解器求解此公式。如果它为您提供了解决方案，则意味着该属性有时会受到侵犯（因为您结合了否定属性）。获得unsat意味着您的模型满足属性/规范。
于 2017-06-11T18:30:04.693 回答
3
为了执行模型检查，需要进行可达性分析，为此，程序转换通常以符号方式执行。由此产生的满意度问题的解决方案由求解器创建。在这本免费教科书（第三部分：分析和验证）中有一个非常基本且非常好的介绍：
Edward A. Lee 和 Sanjit A. Seshia，嵌入式系统简介，网络物理系统方法，第二版，麻省理工学院出版社，ISBN 978-0-262-53381-2，2017
于 2017-05-14T11:55:39.097 回答