| ||||
| ||||
![]() Title:Synthesizing Update-Schedules with Game-Based Extension of Bounded Model Checking Conference:SYNASC 2026 Tags:Bounded Model Checking, Game Theory, Model Checking, Update Scheduling and Updates at Runtime 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. Synthesizing Update-Schedules with Game-Based Extension of Bounded Model Checking ![]() Synthesizing Update-Schedules with Game-Based Extension of Bounded Model Checking | ||||
| Copyright © 2002 – 2026 EasyChair |
