Shielded Learning for Resilience and Performance Based on Statistical Model Checking in Simulink

Safety, resilience and performance are crucial properties in intelligent hybrid systems, in particular if they are used in critical infrastructures or safety-critical systems. In this paper, we present a case study that illustrates how to construct provably safe and resilient systems that still achieve certain performance levels with a statistical guarantee in the industrially widely used modeling language Simulink. The key ideas of our paper are threefold: First, we show how to model failures and repairs in Simulink. Second, we use hybrid contracts to non-deterministically overapproximate the failure and repair model and to deductively verify safety properties in the presence of worst-case behavior. Third, we show how to learn optimal decisions using statistical model checking (SMC-based learning), which uses the results from deductive verification as a shield to ensure that only safe actions are chosen. We take component failures into account and learn a schedule that is optimized for performance and ensures resilience in a given Simulink model.