A Calculus for Hybrid CSP?

Abstract. Hybrid Communicating Sequential Processes (HCSP) is an extension of CSP allowing continuous dynamics. We are interested in applying HCSP to model and verify hybrid systems. This paper is to present a calculus for a subset of HCSP as a part of our efforts in mod-elling and verifying hybrid systems. The calculus consists of two parts. To deal with continuous dynamics, the calculus adopts differential invari-ants. A brief introduction to a complete algorithm for generating poly-nomial differential invariants is presented, which applies DISCOVERER, a symbolic computation tool for semi-algebraic systems. The other part of the calculus is a logic to reason about HCSP process, which involves communication, parallelism, real-time as well as continuous dynamics. This logic is named as Hybrid Hoare Logic. Its assertions consist of tra-ditional pre- and post-conditions, and also Duration Calculus formulas to record execution history of HCSP process