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.
翻译:关于控制器系统与工厂互动的安全的正式推理很复杂,因为开发商需要在考虑到感知不确定性的情况下具体说明行为。 为了解决这个问题,我们建议采用一个自动工作流程,采用不确定性-软件控制器的事件B模型和不确定性作为输入的规格。首先,我们的工作流程将不确定性自动注入原始模型,以获得不确定性意识但可能不安全的控制器。然后,它自动增强控制器,使之即使在不确定的情况下也能满足安全要求。案例研究表明我们的工作流程如何帮助开发商探索多种感知不确定性。我们的结论是,我们的工作流程使得对不确定性意识控制器系统的设计和分析更加容易和系统化。