首页> 外文期刊>Science of Computer Programming >Proving partial-correctness and invariance properties of transition-system models
【24h】

Proving partial-correctness and invariance properties of transition-system models

机译:证明过渡系统模型的部分正确性和不变性

获取原文
获取原文并翻译 | 示例

摘要

We propose an approach for proving partial-correctness and invariance properties of transition systems, and illustrate it on a model of a security hypervisor.Regarding partial correctness, we generalise the recently introduced formalism of Reachability Logic, currently used as a language-parametric logic for programs, to transition systems. We propose a coinductive proof system for the resulting logic, which can be seen as performing an "infinite symbolic execution" of the transition-system model under verification. We embed the proof system in the Coq proof assistant and formally prove its soundness and completeness.The soundness result provides us with a Coq-certified Reachability-Logic prover for transition-system models. The completeness result, although more theoretical in nature, also has a practical value, as it suggests a proof strategy that is able to deal with all valid formulas on a given transition system.The complete proof strategy reduces partial correctness to invariance. For the latter we propose an incremental verification technique for dealing with the case-explosion problem that is known to affect it. All these combined techniques were instrumental in enabling us to prove, within reasonable time and effort limits, that the nontrivial algorithm implemented in a simple hypervisor that we designed in earlier work meets its expected functional requirements. (C) 2019 Elsevier B.V. All rights reserved.
机译:我们提出了一种证明过渡系统的部分正确性和不变性的方法,并在安全管理程序的模型上进行了说明。关于部分正确性,我们归纳了最近引入的可到达性逻辑的形式主义,目前已将其用作语言的参数逻辑。程序,以过渡系统。我们为所得的逻辑提出了一个协合证明系统,可以将其视为执行验证中的过渡系统模型的“无限符号执行”。我们将证明系统嵌入到Coq证明助手中,并正式证明其健全性和完整性。健全性结果为我们提供了经过Coq认证的可过渡性逻辑证明器,用于过渡系统模型。完整性结果虽然在本质上更具理论性,但也具有实用价值,因为它提出了一种证明策略,该策略能够处理给定过渡系统上的所有有效公式。完全证明策略将不变性的部分正确性降低了。对于后者,我们提出了一种增量验证技术,用于处理已知会影响这种情况的案例爆炸问题。所有这些组合技术有助于我们在合理的时间和精力范围内证明我们在早期工作中设计的简单管理程序中实现的非平凡算法可以满足其预期的功能要求。 (C)2019 Elsevier B.V.保留所有权利。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号