Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking
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.