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