Personal tools
You are here: Home Events Title: Verifying safety and persistence properties of hybrid systems

Title: Verifying safety and persistence properties of hybrid systems

— filed under:

Speaker: Paul Jackson

  • Lab Lunch
When Nov 21, 2017
from 01:00 PM to 02:00 PM
Where Mini Forum 2 (MF2) Level 4
Add event to calendar vCal



We propose a method for verifying persistence of nonlinear hybrid systems. Given
some system and an initial set of states, the method can guarantee that system
trajectories always eventually evolve into some specified target subset of the
states of one of the discrete modes of the system, and always remain within this
target region.  The method also computes a time-bound within which the target
region is always reached. The approach combines flow-pipe computation with
deductive reasoning about invariants and is more general than each technique alone.

We illustrate the method with a case study concerning showing that potentially
destructive stick-slip oscillations of an oil-well drill eventually die away for
a certain choice of drill control parameters.  The case study demonstrates how
just using flow-pipes or just reasoning about invariants alone can be
insufficient.  The case study also nicely shows the richness of systems that the
method can handle: the case study features a mode with non-polynomial
(nonlinear) ODEs and we manage to prove the persistence property with the aid of
Paulson?s MetiTarski prover which is specifically designed for handling transcendental

This is joint work with Andrew Sogokon (CMU) and Taylor T. Johnson (Vanderbilt).
It was presented this past May at the 9th NASA Formal Methods Symposium
(NFM 2017).

Document Actions