信息物理系统逻辑基础概述
计算机科学中的逻辑
2021-02-15 v1 编程语言
逻辑
摘要
信息物理系统（CPSs）在计算机技术与物理世界交互时十分重要，正如其在自动驾驶汽车或飞行控制支援系统中所表现的那样。由于其诸多微妙之处，信息物理系统的控制器理应达到最高的正确性标准。其正确运行至关重要，这解释了对其数学模型（称为混合系统，因其结合了离散动力学与连续动力学）的安全性分析技术为何广受关注。微分动态逻辑（dL）为混合系统提供了逻辑规范与严格推理技术。该逻辑 dL 在定理证明器 KeYmaera X 中实现，后者在验证地面机器人控制器、铁路系统以及下一代机载防撞系统 ACAS X 中发挥了关键作用。本章提供了这一 CPS 安全性逻辑方法的非正式概述，该方法在近期教材《信息物理系统逻辑基础》中有详细阐述。它还解释了在已验证模型之境中获得的安全性保证如何完好无损地达到 CPS 执行层面。
引用
@article{arxiv.1910.11232,
title = {Overview of Logical Foundations of Cyber-Physical Systems},
author = {André Platzer},
journal= {arXiv preprint arXiv:1910.11232},
year = {2021}
}