Approximation Based Safety and Stability Verification of Hybrid Systems

Verification;Hybrid Systems;Safety;Stability;Approximations;Polynomial Approximations;Abstraction Refinement;Stability preserving Approximations

Prabhakar, Pavithra

关键词: Verification;    Hybrid Systems;    Safety;    Stability;    Approximations;    Polynomial Approximations;    Abstraction Refinement;    Stability preserving Approximations;   

Others  :  https://www.ideals.illinois.edu/bitstream/handle/2142/26102/Prabhakar_Pavithra.pdf?sequence=1&isAllowed=y

美国|英语

来源: The Illinois Digital Environment for Access to Learning and Scholarship

【 摘 要 】

With the advent of computers to control various physical processes,there has emerged a new class of systems which contain tight interactions between the "discrete" digital world and the"continuous" physical world.These systems which exhibit mixed discrete-continuous behaviors, called "hybrid systems", are present everywhere - in automotives, aeronautics, medical devices, robotics - and are often deployed in safe-critical applications. Hence, reliability of the performance of these systems is a very important issue, and this thesis concerns automatic verification of their models to improve the confidence in these systems.Automatic verification of hybrid systems is an extremely challenging task, owing to themany undecidability results in the literature. Automated verification has been seen to be feasible for only simple classes of systems.These observations have emphasized the need for simplifying thecomplexity of the system before applying traditional verificationtechniques. This thesis explores the feasibility of such an approach for verifying complex systems.In this thesis, we take the approach of verifying a complex system by approximating it to a "simpler" system. We consider two important classes of properties that are required of hybrid systems in practice, namely, "safety" and "stability".Intuitively, safety properties are used to express the fact thatsomething bad does not happen during the execution of the system; and stability is used to capture the notion that small perturbations in the initial conditions or inputs to the system, do not result indrastic changes in the behaviors of the system.For safety verification, we present two techniques forapproximation, an error based technique which allows one to compute as precise an approximation as desirable in terms of a quantified errorbetween the original and the approximate system, and a property based technique which takes into account the property being analysed in constructing and refining the approximate system.With regard to error based approximation, we provide a technique for approximating a general hybrid system to a polynomial hybrid systemwith bounded error. The above technique is in general semi-automatic; and we present afully automatic efficient method for analysing a subclass of hybridsystems by constructing piecewise polynomial approximations.In terms of property based approximation, we propose a novel"counterexample guided abstraction refinement" (CEGAR) techniquecalled "hybrid CEGAR", which constructs a hybrid abstraction ofa system unlike the previous methods which were based on constructing finite state abstractions. Our method has several advantages in terms of simplifying the varioussubroutines in an iteration of the CEGAR loop. We have implemented the hybrid CEGAR algorithm for a subclass of hybrid systems called "rectangular hybrid systems" in a tool called HARE, and the experimental results show that themethod has the potential to scale.Though automated verification of safety properties has been wellstudied, verification of stability properties is still in itspreliminary stages with respect to automation. In this thesis, we present certain foundational results which could potentially be used to develop automated methods for analysis of stability properties. We present a framework for verifying "asymptotic" stability or convergence of (distributed) hybrid systems which operate in discrete steps. We then ask a fundamental question related to approximation based verification, namely, what kinds of simplifications preserve stability properties? It turns out that stability properties are not invariant underbisimulation which is a canonical transformation under which variousdiscrete-time properties (including safety) are known to be invariant. We enrich bisimulation with uniform continuity conditions which suffice to preserve various stability properties. These reductions are widely prevelant in the traditional techniques for stability analysis thereby emphasizing the potentialuse of these techniques for stability verification by approximation.