  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.
