Relational Abstraction
Relational abstraction transforms a hybrid system by replacing
the continuous dynamics in each mode by their summary.
Software Download
A tool for creating relational abstractions of HybridSAL models.
The output is an infinite state SAL model that can be analyzed
using sal-inf-bmc with its various flags.
Download HybridSal.tgz from here (updated new version on Feb 06, 2015).
Download win32_HybridSal.tgz from here for the Cygwin (windows) version (updated Dec, 2014).
Instructions for installing, examples, documentation, etc.
can be found in the directory HybridSal; see the file README to get started.
Documentation
Preferably see the documentation in the doc/ subdirectory under the directory HybridSal.
One version of the
documentation is here.
Slides describing the HybridSAL relational abstractor can be found
here.
HybridSal Examples
See examples in the examples/ subdirectory under the directory HybridSal.
HybridSal files have a suffix .hsal.
The directory contains examples used in a submission to CAV 15.
The examples are also included in the HybridSal release (.tgz) above.
The directory
contains files that
can be used to create linear hybrid system models
of collision avoidance for multiple vehicles
. Documentation and results describing the model
and its analysis are forthcoming.
Here is a
simple example illustrating relational abstraction.
A simple example of a switched hybrid system is
the LCR circuit controlled by a switch.
Switch open mode:
d V_C/dt = 5 - V_C - V_L,
d V_L/dt = -5 + V_C -V_L
Switch closed mode:
d V_C/dt = 5 - 3 V_C - V_L,
d V_L/dt = -5 + 3 V_C - V_L$
Switch from open to closed mode when Vc in [4.5,5.5]
Switch from closed to open mode when Vc in [1,2]
The relational abstraction of this model can be
found in lcr.sal.
Relational Abstraction of Navigation Benchmarks
Benchmarks for verification of hybrid systems can be downloaded from
here .
We used some of the navigation benchmarks from the above
to test the value of
the idea of relational abstractions.
The
nav.sal
contains the relational abstractions of the nav01--nav10
benchmarks, along with the safety properties and auxiliary
lemmas, whenever they were needed.
Under the assumption that the NAV01-NAV06 examples spend
atleast 1/10 second in every mode, we generate a stronger
relational abstraction, which can be found in
the file navZeno.sal
The relational invariants in nav.sal were generated using
redlog/qepcad quantifier elimination (see below) procedure.
The
nav.red is a reduce-redlog script
that was used to generate the invariants used in nav.sal.
The current version of the tool can automatically generate
the relational abstraction for linear hybrid systems (such
as nav benchmarks). There is no need for QE tools (below).
Quantifier Elimination Tools
If trying to analyze nonlinear hybrid systems using relational
abstraction, you will need to create the relational abstraction
using QE tools.
Here are some freely available tools that can be used
to compute relational abstractions -- they provide
quantifier elimination and simplification capabilities.
Publications
Related to HybridSal and Relational Abstraction:
Other papers (unrelated to HybridSal)
Acknowledgments
This material is based upon work supported in part
by the National Science Foundation, NASA, and Darpa under various grants.
Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the funding agencies.
This page is maintained by Ashish Tiwari.
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page