Modelling and Verification of Hybrid Systems
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.
Prof. Chaochen ZHOU
Date & Time
28 Jul 2011 (Thursday) 15:00
Department of Computer and Information Science
ZHOU Chaochen is a research professor of Institute of Software. He was interested in distributed programming theory in 1980s, and received a second class award for China natural science research in 1987. In 1991, he turned his interest to real-time systems, and jointly with Professors Hoare and Ravn proposed a continuous-time interval logic called Duration Calculus. Currently, he is interested in the interdisciplinary subject – Modelling and Verification of Hybrid Systems. From Aug. 1992 to Sep. 2002, he served as the principal research fellow and then the director of the International Institute for Software Technology, United Nations University. In 1993, he was elected Member of Chinese Academy of Sciences.