Abstract

An hybrid system includes continuous dynamics to describe behaviour of physical device and computers to control the device. Hybrid system is widely used, and its safety is quite often required. We propose a formal approach to modelling and verification of hybrid systems. This approach uses Hybrid Communicating Sequential Processes (HCSP) to model hybrid systems, and Differential Invariants to interpret continuous dynamics. The approach also establishes a calculus, called Hybrid Hoare Logic (HHL), to reason about HCSP models. In HHL an assertion consists of traditional pre- and post-conditions, and a Duration Calculus formula to record execution history of HCSP processes. Following this approach, one of our on-going project attempts at modelling and verifying the scenarios specified in the Level 3 of Chinese Train Control System (CTCS-3). This talk gives a brief introduction to HCSP, differential invariants and a complete algorithm for generating polynomial differential invariants, which is supported by a symbolic computation tool, DISCOVERER, and also to an improved HHL calculus, the original one is published in LNCS 6461.