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

Adelt J.; Bruch S.; Herber P.; Niehage M.; Remke A.

Zusammenfassung

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.