Formal modelling, analysis and verification of hybrid systems

Abstract. Hybrid systems is a mathematical model of embedded sys-tems, and has been widely used in the design of complex embedded sys-tems. In this chapter, we will introduce our systematic approach to formal modelling, analysis and verification of hybrid systems. In our framework, a hybrid system is modelled using Hybird CSP (HCSP), and specified and reasoned about by Hybrid Hoare Logic (HHL), which is an exten-sion of Hoare logic to hybrid systems. For deductive verification of hy-brid systems, a complete approach to generating polynomial invariants for polynomial hybrid systems is proposed; meanwhile, a theorem prover for HHL that can provide tool support for the verification has been im-plemented. We give some case studies from real-time world, for instance, Chinese High-Speed Train Control System at Level 3 (CTCS-3). In ad-dition, based on our invariant generation approach, we consider how to synthesize a switching logic for a considered hybrid system by reduction to constraint solving, to meet a given safety, liveness, optimality require-ment, or any of their combinations. We also discuss other issues of hybrid systems, e.g., stability analysis