Beyond HyTechStructure of this talkHybrid automataSymbolic model checkingHyTechHyTech cont.Shortcomings of HyTechCurrent ways to avoid shortcomingsAvoiding shortcomings, cont.Massaging input, cont.Our objectiveInterval numerical methodsHyTech’s algorithmOur algorithmComputing time successorsExample: thermostatTighter bounds for thermostatNuclear reactorFuture workBeyond HyTechPresented by:Ben Horowitz and Rupak Majumdar{bhorowit,rupak}@eecs.berkeley.eduJoint work with Tom Henzinger and Howard Wong-Toi.Structure of this talkHybrid automataSymbolic model checkingHyTechInterval numericsHyTech’s algorithmExtending HyTech’s dynamicsThermostat exampleHybrid automata(V, E, X, pre, post, init, flow, jump, inv, Σ)Symbolic model checkingState 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.HyTechSymbolic 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 HyTechHyTech allows only restrictive dynamics:polyhedral automataFor example, in the cutoff control study:dynamics required extensive manual approximation before HyTech could be applied.Current ways to avoid shortcomingsFor 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!State explosion!Our objectiveOur 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 methodsArithmetic 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 algorithmMaintain 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 S,add non-visited successors to R’,R := R { r }.Maintain two sets of regions:R : already-explored region,R’ : to-be-explored region.Initially, R = and R’ is the initial region.while (R’):remove region r from R’,compute r’s event and time successors S,add non-visited successors to R’,R := R { r }.Our algorithmrComputing time successorsStart with:exit region e,initial rectangle r.Use interval numerical integration to compute time successors of r.Stop when we hit e.eExample: thermostatTighter bounds for thermostatUsing HyTech, it was shown that0 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 reactorExample from [ACHH].HyTech with old algorithm givest = 2 for controllability.New Algorithm gives t = 1.55.Other (small) examples in the HyTech example suite also work.Future workTry larger examples, e.g. cutoff control.Investigate whether interval numerical methods can be used on polyhedra or ellipsoids.Redesign HyTech’s input language and
View Full Document
Unlocking...