Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty
Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty
复制标题
DOI：
10.1007/978-3-030-76384-8_13
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
Tsutomu Kobayashi;Rick Salay;I. Hasuo;K. Czarnecki;F. Ishikawa;Shin-ya Katsumata
中科院分区：
文献类型：
--
作者：
Tsutomu Kobayashi;Rick Salay;I. Hasuo;K. Czarnecki;F. Ishikawa;Shin-ya Katsumata
与植物相互作用的控制器系统的安全性的形式化推理是复杂的，因为开发人员需要指定的行为，同时考虑到感知的不确定性。为了解决这个问题，我们提出了一个自动化的工作流程，需要一个事件B模型的不确定性不知道控制器和规范的不确定性作为输入。首先，我们的工作流程自动将不确定性注入到原始模型中，以获得一个不确定性感知但可能不安全的控制器。然后，它自动鲁棒控制器，使其满足安全，即使在不确定性。案例研究展示了我们的工作流程如何帮助开发人员探索多层次的感知不确定性。我们的结论是，我们的工作流程使设计和分析的不确定性感知控制器系统更容易，更系统。
Formal reasoning on the safety of controller systems interacting with plants is complex because developers need to specify behavior while taking into account perceptual uncertainty. To address this, we propose an automated workflow that takes an Event-B model of an uncertainty-unaware controller and a specification of uncertainty as input. First, our workflow automatically injects the uncertainty into the original model to obtain an uncertainty-aware but potentially unsafe controller. Then, it automatically robustifies the controller so that it satisfies safety even under the uncertainty. The case study shows how our workflow helps developers to explore multiple levels of perceptual uncertainty. We conclude that our workflow makes design and analysis of uncertainty-aware controller systems easier and more systematic.