Synthesizing Switching Logic using Constraint Solving

Synthesizing Switching Logic using Constraint Solving

Ankur Taly (Stanford), Sumit Gulwani (Microsoft Research) and Ashish Tiwari (SRI Intl.)

Abstract

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 $\exists\forall$ formula in the theory of reals, which we solve using SMT solvers. The generated controlled invariant is then used to arrive at the maximally liberal switching logic.

pdf

BibTeX Entry



@inproceedings{TGT09:VMCAI,
	title= "Synthesizing Switching Logic using Constraint Solving",
	author = "Taly, A. and Gulwani, S. and Tiwari, A.",
	booktitle = "Proc. 10th Intl. Conf. on Verification, Model Checking and Abstract Interpretation, VMCAI",
	year = 2009,
	pages = "305--319",
	publisher = "Springer",
	volume = 5403,
	series = "{LNCS}",
}

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page