Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty
This addresses safety specification problems for developers of cyber-physical systems, but it appears incremental as it builds on existing formal methods like Event-B.
The paper tackles the challenge of ensuring safety in cyber-physical systems with perceptual uncertainty by proposing an automated workflow that robustifies controller specifications, making design and analysis easier and more systematic.
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.