Abstract Autonomous hybrid systems are systems that combine discrete and continuous behavior with autonomous decision-making, e.g., using reinforcement learning. Such systems are increasingly used in safety-critical applications such as self-driving cars, autonomous robots or water supply systems. Thus, it is crucial to ensure their safety and resilience, i.e., that they function correctly even in the presence of dynamic changes and disruptions. In this paper, we present an approach to obtain formal resilience guarantees for autonomous hybrid systems using the interactive theorem prover KeYmaera X. Our key ideas are threefold: First, we derive a formalization of resilience that is tailored to autonomous hybrid systems. Second, we present reusable patterns for modeling stressors, detecting disruptions, and specifying resilience as a service level response in the differential dynamic logic (d $$\mathcal {L}$$ L ). Third, we combine these concepts with an existing approach for the safe integration of learning components using hybrid contracts, and extend it towards dynamic adaptations to stressors. By combining reusable patterns for stressors, observers, and adaptation contracts for learning components, we provide a systematic approach for the deductive verification of resilience of autonomous hybrid systems with reduced specification effort. We demonstrate the applicability of our approach with two case studies, an autonomous robot and an intelligent water distribution system.

Abstract In embedded systems, the execution semantics of the real-time operating system (RTOS), which is responsible for scheduling and timely execution of concurrent processes, is crucial for the correctness of the overall system. However, existing approaches for the formal verification of embedded systems typically abstract from the RTOS completely, or provide a detailed and synthesizable formal model of the RTOS. While the former may lead to unsafe systems, the latter is not compatible with industrial design processes. In this paper, we present an approach for reusable abstract formal models that can be configured for custom RTOS. Our key idea is to formally capture common execution mechanisms of RTOS like preemptive scheduling, event synchronization, and communication abstractly in configurable timed automata models. These abstract formal models can be configured for a concrete custom RTOS, and they can be combined into a formal system model together with a concrete application. Our reusable models significantly reduce the manual effort of defining a formal model that captures concurrency and real-time behavior, together with the functionality of an application. The resulting formal model enables analysis, verification, and graphical simulation. We validate our approach by formalizing and analyzing a rescue robot application running the custom open source RTOS EV3RT.