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 modelling and verifying hybrid systems. The calculus consists of two parts. To deal with continuous dynamics, the calculus adopts differential invariants. A brief introduction to a complete algorithm for generating polynomial 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 traditional pre- and post-conditions, and also Duration Calculus formulas to record execution history of HCSP process. © 2010 Springer-Verlag.
CITATION STYLE
Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., & Zou, L. (2010). A calculus for hybrid CSP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6461 LNCS, pp. 1–15). https://doi.org/10.1007/978-3-642-17164-2_1
Mendeley helps you to discover research relevant for your work.