Tenth and final Meeting
- John Rushby
-
Title: Analysis of Infinite State and Hybrid Systems with SAL
(
Slides)
- Abstract:
will give an overview of work performed by my colleagues.
SAL is a modeling notation similar to PVS but specialized for state
machines; it is supported by several high-performance model checkers.
ICS is a highly efficient integration of a SAT solver with a standalone
implementation of decision procedures comparable to those in PVS.
One of the SAL tools performs bounded model checking and verification by
k-induction for systems whose state variables are drawn from the
theories decided by ICS (which include the reals). This "infinite
bounded model checker" can analyze several classes of infinite state
systems, including timed automata.
Hybrid SAL adds a notation for derivatives and is supported by Hybrid
Abstraction, which is a method for constructing discrete approximations
to hybrid systems. It works by abstracting polynomials over real
variables and their derivatives to their qualitative signs. The
abstraction is fully automated using an efficient, though incomplete
decision procedure for real closed fields. The discrete approximation
can be analyzed using the conventional model checkers of SAL and the
overall procedure has been used to perform reachability analysis on
hybrid systems with more than 10 continuous variables.