Synthesizing safe fixed update schedules for critical systems
Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking
Computer Science and Game TheoryLogic in Computer Science
Summary
Updating software in important systems like self-driving cars is tricky because you want to keep the system running without interruption. The authors create a way to plan updates at specific times so that the update is always safe, no matter how the system behaves on its own. They treat the update process as a game between the system and the updater and use logical methods to find schedules that work. They tested their approach on a self-driving car’s path planner to show it can safely update under all allowed situations.
What this means in practice
- •For autonomous vehicle engineers: Generate fixed-time update plans that guarantee safe software deployment without halting autonomous driving systems.
- •For industrial control system operators: Create guaranteed safe update schedules that maintain continuous operation of safety-critical equipment without spare hardware.
Authors
Janis Kröger, Paul Kröger, Martin Fränzle
Abstract
Ensuring safe software updates in safety-critical systems without interrupting operation and without provisioning and activating cold spare hardware poses a fundamental challenge due to the conflict between system availability and update execution. In this paper, we present a bounded SMT encoding for synthesizing fixed global-time update schedules for timed-games with linear update automata and a fixed number of update transitions. We model the interaction between the system and the update as a two-player timed game. Our key contribution is the synthesis of global time points that define a fixed update schedule which guarantees safe and complete deployment of the update independently of the autonomous system behavior. To this end, we reduce the scheduling problem to a reachability and safety objective and encode it as a quantified SMT problem. We demonstrate it on an example system of a trajectory planner for autonomous driving, showing that the synthesized schedule ensures safe deployment under all admissible executions.