The Formal Analysis And Verification Of Hybrid System Based On Hierarchical Analysis

The evolution of electronics, as well as the requirements of human activities, makes computer related technologies involving in each field of engineering, widely and deeply, e.g., the reason of why the hybrid systems, characterized by both discrete and continuous behaviors, are common now. We study the hybrid system in a formal way. The formal methods of hybrid system contain formal analysis, formal verification and validation, all of which are based on calculus and hybrid automata generally. The theories of these calculus or automata are well-studied and extended, but modeling is now a challenge.Control system, embedded system and cyber physical system belong to hy-brid systems, each of them adopts hierarchical methodology while designing. Then it is basic and significant to quickly generate the accurate formal model from these hierarchical designs.In this thesis, we try to find a direct theoretical way that maps the hierar-chical designs into the formal model of hybrid system, e.g., with a widely used hierarchical design model[24], we symbolize the hierarchical design and get the hierarchial formal model. Then we study the semantics of both duration calculus and hybrid automata based on the hierarchical formal model, and then study the way of analysis and validation with some practical case studies.