用于基于SMT的验证的Scade模型转换

Henning Basold

用于基于SMT的验证的Scade模型转换

计算机科学中的逻辑 2014-03-13 v1

作者: Henning Basold

摘要

在本工作中，我们开发了一种针对 Scade 程序安全性质的完全自动验证程序。我们将每个此类程序转换为一个 SMT 实例（Satisfiability Modulo Theories）并将其输入求解器。目标是提供一个公开可访问的 Scade 程序验证实验平台。选择 SMT 的原因在于，与命题逻辑相比，它提供了表达能力更强的逻辑，且其求解器已被证明性能优异。SMT 逻辑的表达能力使我们能够实现符号模型检测，从而避免在验证过程中展开模型的完整状态空间。为了降低复杂性，我们分两步将 Scade 程序转换为 SMT 实例。首先，将它们归约为同步数据流语言 Lama 的程序。该语言的语义比 Scade 更简单，同时仍保留了程序员的某些抽象。接下来，我们将这样的 Lama 程序解释为一个无量词的一阶公式系统。Lama 中剩余的抽象可用于简化这些系统。这反过来可以加快验证过程，并允许验证更多性质。我们使用 Haskell 在软件中成功实现了这些转换。本工作最后将该软件与 Scade Suite 自带的现有验证软件“Scade Design Verifier”进行了比较。

关键词

Scade SMT 形式化验证符号模型检测同步数据流安全性质

引用

@article{arxiv.1403.2752,
  title  = {Transformation von Scade-Modellen zur SMT-basierten Verifikation},
  author = {Henning Basold},
  journal= {arXiv preprint arXiv:1403.2752},
  year   = {2014}
}

备注

The implementation can be found at https://github.com/hbasold/LAMA

用于基于SMT的验证的Scade模型转换

摘要

关键词

引用

备注

相关论文