Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty

TL;DR

This paper presents an automated workflow that enhances controller models with perceptual uncertainty considerations, ensuring safety despite uncertainties in cyber-physical systems.

Contribution

It introduces a novel automated process to inject and robustify uncertainty in controller models, improving safety analysis in cyber-physical systems.

Findings

Workflow successfully injects uncertainty into models

Robustified controllers maintain safety under uncertainty

Facilitates systematic exploration of perceptual uncertainties

Abstract

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.