合约的机械验证理论
摘要：网络-物理系统（CPS）是由网络，异构硬件和软件组件组成的，这些组件感知、评估和操控物理环境。这种异质性引发了复杂性，使得CPS的正确建模变得具有挑战性。由于CPS通常具有关键功能，因此形式化验证它们以提供最高的安全保障非常重要。面对CPS的复杂性，模型抽象变得至关重要，以实现可验证性。为此，假设/保证合约可以通过组件模型抽象来支持一种完整、结构化和模块化的验证过程。虽然通常可以证明合同模型的抽象是正确的，但据我们所知，迄今为止还没有证明相关的合同框架本身是正确的。为此，我们在Coq证明助手中提出了一个通用的假设/保证合约理论的形式化。我们确定并证明了确保其正确性的定理。我们的理论是通用的，或者说参数化的，因为它可以与任何给定的逻辑一起实例化和使用，特别是可以统一描述高度复杂的网络-物理系统的混合逻辑。
作者：St''ephane Kastenbaum (MERCE-France, TEA), Beno^it Boyer (MERCE-France), Jean-Pierre Talpin (TEA)
论文ID：2108.13647
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2021-09-01