A bounded model checking tool for periodic sample-hold systems

Safety verification of a plant together with its controller is an important part of controller design. If the controller is implemented in software, then a formal model such as hybrid automata is needed to model the composite system. However, classic hybrid automata scale poorly for complex software controllers due to their eager representation of discrete states. In this paper we present safety verification for software controllers without constructing hybrid automata. Our approach targets a common class of software controllers, where the plant is periodically sampled and actuated by the controller. The resulting systems exhibit a regular alternation of discrete steps and fixed length continuous-time evolution. We show that these systems can be verified by a combination of SMT solving and Taylor models. SMT formulas accurately capture control software in a compact form, and Taylor models accurately capture continuous trajectories up to guaranteed error bounds.