本文使用差异动态逻辑的形式主义,为对网络物理系统的有限传感器攻击进行定量分析。鉴于系统的前提和后结构,我们将两个定量安全性,定量的前进和后部安全性形式化,分别表达(1)该系统对指定后条件的最强后条件的强大程度,以及(2)指定的预先对系统的强度确保所需的最弱的预先条件,以确保系统的最弱点。我们介绍了两个概念,即前进和向后的鲁棒性,以将系统抗攻击的鲁棒性描述为安全性丧失。两个模拟距离分别表征了由传感器攻击引起的前向和向后安全损失程度的上限,以符合稳定性。我们通过将两个模拟距离作为差分动态逻辑的公式表达出来,并在现有工具支持的情况下证明公式。我们展示了需要避免碰撞的自动驾驶汽车的例子。
主要关键词