通过自动证明迈向成员系统的验证
软件工程
2014-05-09 v2
摘要
本文探讨了在面向系统之系统（Systems of Systems, SoS）的 Symphony 工具平台背景下成员系统的验证。我们的 SoS 建模语言 CML 支持多种契约式规约元素，例如状态不变式与操作前置条件，这些元素可用于对 SoS 的成员系统规定契约义务。为了支持这些义务的验证，我们为 Symphony 开发了证明义务生成器和定理证明插件。后者使用 Isabelle/HOL 定理证明器来自动消解由 CML 模型产生的证明义务。我们希望由此产生的证明随后可用于形式化验证每个成员系统的一致性，进而构建出可靠的 SoS。
引用
@article{arxiv.1404.7792,
title = {Towards Verification of Constituent Systems through Automated Proof},
author = {Luis Diogo Couto and Simon Foster and Richard Payne},
journal= {arXiv preprint arXiv:1404.7792},
year = {2014}
}
备注
EDCC-2014, EDSoS-2014