Synthesizing Switching Logic Using Constraint Solving

A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a given form. In this paper, we extend that work to automatic synthesis of safe hybrid systems. Starting with a multi-modal dynamical system and a safety property, we present a sound technique for synthesizing a switching logic for changing modes so as to preserve the safety property. By construction, the synthesized hybrid system is well-formed and is guaranteed safe. Our approach is based on synthesizing a controlled invariant that is sufficient to prove safety. The generation of the controlled invariant is cast as a constraint solving problem. When the system, the safety property, and the controlled invariant are all expressed only using polynomials, the generated constraint is an ∃∀ formula in the theory of reals, which we solve using SMT solvers. The generated controlled invariant is then used to arrive at...

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Ankur Taly, Sumit Gulwani, Ashish Tiwari
• Keywords: Controlled Invariant, Hybrid System, Safety Property, Software Engineering, VMCAI 2009