Beyond HyTech Presented by Ben Horowitz and Rupak Majumdar bhorowit rupak eecs berkeley edu Joint work with Tom Henzinger and Howard Wong Toi Structure of this talk Hybrid automata Symbolic model checking HyTech Interval numerics HyTech s algorithm Extending HyTech s dynamics Thermostat example Hybrid automata V E X pre post init flow jump inv Symbolic model checking State space of a hybrid automaton is infinite Thus verification algorithms must be symbolic To have a symbolic algorithm we need finite representation of infinite state sets Pre Boolean operations as primitives on state sets HyTech Symbolic model checker for hybrid automata Automata must be polyhedral flow conditions are polyhedra invariants pre post etc are also polyhedra state sets are unions of convex polyhedra Pre implemented as polyhedral manipulation HyTech cont HyTech has been used to verify several realistic examples audio control protocol steam boiler auto engine in cutoff controller mode Shortcomings of HyTech HyTech allows only restrictive dynamics polyhedral automata For example in the cutoff control study dynamics required extensive manual approximation before HyTech could be applied Current ways to avoid shortcomings For a large system one may Simulate via numerical integration not appropriate for verification may miss events round off errors Massage into HyTech acceptable form messy time consuming Avoiding shortcomings cont Massaging input with rate translation Replace nonlinear x with linear x Bound d dt x by upper lower constants Split location v into several locations to yield better approximation Massaging input cont Thermostat becomes State explosion Our objective Our aim is to provide both a more direct and a more accurate analysis of hybrid systems More direct dynamics may be modeled directly More accurate bounds obtained are tighter We have implemented a prototype Interval numerical methods Arithmetic operators on intervals instead of reals 2 7818 3 1416 Numerical ODE solvers available ODE solutions lie within validated intervals In worst case solution is unacceptably wide But solution is never false HyTech s algorithm Maintain two sets of regions R already explored regions R to be explored regions Initially R and R is the initial region while R remove region r from R compute r s event and time successors add non visited successors to R R R r Our algorithm Maintain two sets of regions R already explored region R to be explored region Initially R and R is the initial regio while R remove region r from R compute r s event and time successors S add non visited successors to R R R r Computing time successors r Start with e exit region e initial rectangle r Use interval numerical integration to compute time successors of r Stop when we hit e Example thermostat Tighter bounds for thermostat Using HyTech it was shown that 0 x 4 Using a 20 state approximation HyTech obtains the bounds 28 x 3 76 Using interval numerical methods the new HyTech shows that 367 x 3 64 Nuclear reactor Example from ACHH HyTech with old algorithm gives t 2 for controllability New Algorithm gives t 1 55 Other small examples in the HyTech example suite also work Future work Try larger examples e g cutoff control Investigate whether interval numerical methods can be used on polyhedra or ellipsoids Redesign HyTech s input language and implementation
View Full Document
Unlocking...