Algorithmic Analysis Of Hybrid System

Hybrid system is suitable for capturing the interaction between discrete componentsand continuous components in embedded systems. It bridges the big gap betweencomputer science, control engineering and mathematics; it also provides formalanalysis and synthesis of embedded systems.Formal verification is an important approach to analysis of hybrid systems. The safetyof systems can be guaranteed by formal verification. Reachability analysis andcomputation of reachable set consist of the foundation of formal verification of hybridsystems.The major researches of this thesis are as follows:1. A forward reachability algorithm is designed for the analysis of hybrid systems. The correctness validation of forward reachability algorithm is also given. Then the algorithm is constructed and implemented in ReachLab. By using the translator of ReachLab, the algorithm model can be translated into executable Matlab code.2. Symbolic computation is introduced to get the exact reachable set of a specified hybrid system. Reachable sets of hybrid systems can be represented by symbolic approach. Quantifier elimination is used to eliminate the existential and/or universal quantifier for exact reachable set of hybrid systems.3. Based on the exact reachable set obtained by symbolic computation, an approach to error analysis is defined.