Verified Runtime Validation for Partially Observable Hybrid Systems
Verified Runtime Validation for Partially Observable Hybrid Systems
复制标题
部分可观测混合系统的运行时验证
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
André Platzer
中科院分区：
文献类型：
--
作者：
Stefan Mitsch;André Platzer
形式化验证提供了强有力的安全保证，但仅限于网络物理系统的模型。混合系统模型描述了计算和物理动力学所需的相互作用，这对于保证哪些计算导致安全的物理行为（例如，汽车不应该碰撞）至关重要。影响物理动力学的控制计算必须提前采取行动，以避免可能不安全的未来情况。然后，形式验证确保控制器在特定物理模型下正确识别并可证明地避免不安全的未来情况。但是，任何物理模型都必然偏离现实，而且，任何用真实传感器进行的观察和用真实驱动器进行的操作都受到不确定性的影响。这使得运行时验证成为监视模型假设是否适用于实际系统实现的关键步骤。
Formal verification provides strong safety guarantees but only for models of cyber-physical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe future circumstances. Formal verification then ensures that the controllers correctly identify and provably avoid unsafe future situations under a certain model of physics. But any model of physics necessarily deviates from reality and, moreover, any observation with real sensors and manipulation with real actuators is subject to uncertainty. This makes runtime validation a crucial step to monitor whether the model assumptions hold for the real system implementation.
The key question is what property needs to be runtime-monitored and what a satisfied runtime monitor entails about the safety of the system: the observations of a runtime monitor only relate back to the safety of the system if they are themselves accompanied by a proof of correctness! For an unbroken chain of correctness guarantees, we, thus, synthesize runtime monitors in a provably correct way from provably safe hybrid system models. This paper addresses the inevitable challenge of making the synthesized monitoring conditions robust to partial observability of sensor uncertainty and partial controllability due to actuator disturbance. We show that the monitoring conditions result in provable safety guarantees with fallback controllers that react to monitor violation at runtime.
护盾合成
影响因子：
0.8
作者：
Alshiekh, Mohammed;Bloem, Roderick;Humphrey, Laura;Topcu, Ufuk;Wang, Chao
通讯作者：
Wang, Chao