一种经机械验证的契约理论
形式语言与自动机理论
2021-09-01 v1
摘要
信息物理系统(CPS)是由联网的、异构的硬件与软件组件构成的集合，这些组件感知、评估并驱动物理环境。这种异构性引入了复杂性，使得 CPS 难以被正确建模。由于 CPS 常具关键功能，为提供最高级别的安全性保障，对其形式化验证至关重要。面对 CPS 的复杂性，模型抽象成为使验证可行的关键。为此，假设/保证契约支持组件模型抽象，以支撑可靠、结构化且模块化的验证过程。尽管基于契约的模型抽象通常被证明是可靠的，但据我们所知，现有相关契约框架本身迄今均未经过形式化正确性证明。为此，我们在证明辅助工具 Coq 中给出了通用假设/保证契约理论的形式化。我们识别并证明了确保其正确性的定理。我们的理论是通用的，或参数化的，可被实例化并与任意给定逻辑（特别是可统一描述高度复杂信息物理系统的混合逻辑）配合使用。
引用
@article{arxiv.2108.13647,
title = {A Mechanically Verified Theory of Contracts},
author = {Stéphane Kastenbaum and Benoît Boyer and Jean-Pierre Talpin},
journal= {arXiv preprint arXiv:2108.13647},
year = {2021}
}