Supervisor synthesis for controller upgrades

During the life cycle of a cyber-physical system, it is sometimes necessary to upgrade a working controller with a new, but unverified, one which provides better performance or additional functionality. To make sure that system invariants are not broken because of bugs in the new controller, an architecture is used in which both controllers are implemented on the platform, and a supervisor process checks that the actions of the new controller keep the system within its safe states. If an invariant may be violated, the supervisor switches over to the old controller that ensures correct behavior, but possibly degraded performance. A key question in the design of such supervisors is the switching strategy: when should the supervisor reinstate the new controller after it has switched to the old one? In general, one would prefer to use the new controller as much as possible, provided it does not violate safety. However, arbitrarily switching back to the new controller can cause the system to become unstable, even when each controller in isolation ensures stability. We provide a supervisor synthesis procedure that uses a simple counting strategy for the supervisor. Our synthesized supervisor ensures that switching between the controllers ensures stability of the system, while maintaining its safety properties and providing a lower bound on the use of the new controller. We prove the correctness of the strategy and show on an example that it can provide close to optimal use of the new controller against many disturbance scenarios.