Verification of Hybrid Systems An Assessment of Current Techniques Holly Bowen Verification Methods Formal verification – determining whether given properties are true for a given model of a dynamic system Theorem proving – inferring/contradicting a specification using logical proof systems Not restricted to finite-state systems Model checking – using the state-transition relation in iterative computations to arrive at the set of states for which the specification is true Algorithmic technique Model Checking Requires the construction of a finite-state approximation of the continuous dynamics Verification of properties for the finite-state approximation may be inconclusive! E.g. if a state is reachable in the finite-state approximation, that doesn’t imply it is reachable in the underlying hybrid system Tools can refine the approximation, but refinement will not necessarily terminate Example: Batch Reactor System Discrete controller: vA, vB, vC, vO Variables: TR, VR, tR, cA Exothermic reaction: 2A + B D Operation Procedure Formal verification: Are the forbidden states (z5, z6) reachable? Hybrid Model of System Model Checking Tools UPPAAL HYTECH d/dt CheckMate VERDICT UPPAAL Systems are represented as networks of timed automata (TA) Can analyze simple liveness properties and reachability properties Uses clock difference diagrams to represent TA in a compact format User must manually translate the process behavior into a set of concurrent TA UPPAAL reactor behavior Desired states: S2, S5, S9 Result: S10 is reachable! operation procedure HYTECH Specifications are given as temporal logic expressions Uses symbolic model checking in the continuous state space Can only model flows with form A x B (linear hybrid automata) HYTECH Three approaches to verify systems of higher complexity than LHA: Clock transition models – continuous state variables are replaced by clock variables (pure integrators with different rates) • Constraints identify regions for which given rates are valid Rate translation – Retains original state variables, but approximates continuous behavior with piecewiseconstant bounds on first derivatives Linear phase-portrait approximation – Derivatives of state variables can be constrained in linear combinations • Gives a better approximation to original state equations Rate Translation d/dt Performs reachability analysis for hybrid systems with linear continuous dynamics Face-lifting – computing collections of orthogonal polyhedra to represent reachable sets Allows models with uncertainty in the input in the dynamics equations E.g. x Axlinearize Bu , u U system dynamics around the User must operating point of interest Face Lifting Each face is moved by an amount that bounds all possible trajectories starting on the face CheckMate MATLAB-based tool, handles systems with arbitrary nonlinear continuous dynamics Allows any Simulink/StateFlow blocks for simulation Verification: Logical operators (AND, OR, XOR, etc.) MUX/DEMUX Switched Continuous System Block (SCSB) Polyhedral Threshold Block (PTHB) Finite State Machine Block (FSMB) CheckMate Computes finite-state approximation using general polyhedral over-approximation to sets of reachable states for continuous dynamics Can refine current approximation and attempt verification again if result is inconclusive Searches for states that led to failure, splits them, recomputes reachable states, evaluates logic expression again CheckMate PHTBs Controller (FSMB) CheckMate c 0 .2 within 1 hour? VERDICT Modular modelling/verification of timed/hybrid systems Structure of system is built in a modular manner Behavior of each module is described by a discrete, timed, or hybrid transition system Translates the model into the input languages of different model checkers for discrete/timed automata HYTECH, KRONOS, SMV, UPPAAL VERDICT hybrid behavior controller Comparisons Two key issues: Computation takes hours – only very small systems can be verified! • Modularity: break systems down into smaller pieces Interpretation of results – cause of failure is not clear Making Tools Useful for Industry Connecting with Existing Models Tools for Exploring Models and Results Model-building process is time-consuming, could introduce errors Useful results are obtained only when the user is directing the verification process Tools for Building Verification Specifications & Interpreting Results Difficult to translate requirement specifications into formal specifications to be verified

Descargar
# Verification of Hybrid Systems