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 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.
This work is supported in part by the projects NSFC-60721061, NSFC-90718041, NSFC-60736017, NSFC-60970031, NSFC-60634010 and RCS2008K001.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Apt, K., de Boer, F., Olderog, E.-R.: Verfication of Sequential and Concurrent Programs. Springer, Heidelberg (2009) ISBN 978-1-184882-744-8
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, Springer, Heidelberg (2008)
: From CSP to hybrid systems. In: The proc. of A Classical Mind: Essays in Honour of C. A. R. Hoare. International Series In Computer Science, pp. 171–189. Prentice-Hall, Englewood Cliffs (1994), ISBN:0-13-294844-3
Liu, J., Zhan, N., Zhao, H.: A complete method for generating polynomial differential invariants. Technical Report of State Key Lab. of Comp. Sci., ISCAS-LCS-10-15 (2010)
Manna, Z., Pnueli, A.: Models of reactitivity. Acta Informatica 30(7), 609–678 (1993)
Olderog, R.-R., Dierks, H.: Real-Time Systems: Formal Secification and Automatic Verification. Cambridge University Press, Cambridge (2008)
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. of Logic and Computation 20(1), 309–352 (2010)
Platzer, A.: Differential dynamic logic for hybrid systems. J. of Automated Reasoning 41, 143–189 (2007)
Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176–189. Springer, Heidelberg (2008)
Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539–554. Springer, Heidelberg (2004)
Xia, B.: DISCOVERER: A tool for solving semi-algebraic systems. In: Software Demo at ISSAC 2007, Waterloo, July 30 (2007); Also: ACM SIGSAM Bulletin 41(3),102–103 (September 2007)
Yang, L.: Recent advances on determining the number of real roots of parametric polynomials. J. Symbolic Computation 28, 225–242 (1999)
Yang, L., Hou, X., Zeng, Z.: A complete discrimination system for polynomials. Science in China (Ser. E) 39, 628–646 (1996)
Zhou, C., Wang, J., Ravn, A.: A formal description of hybrid systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, Springer, Heidelberg (1996)
Zhang, S.: The General Technical Solutions to Chinese Train Control System at Level 3 (CTCS-3). China Railway Publisher (2008)
Zhou, C., Hansen, M.: Duration Calculus: A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004), ISBN 3-540-40823-1
Zhou, C., Hoare, C.A.R., Ravn, A.: A calculus of durations. Information Processing Letters 40(5), 269–276 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, J. et al. (2010). A Calculus for Hybrid CSP. In: Ueda, K. (eds) Programming Languages and Systems. APLAS 2010. Lecture Notes in Computer Science, vol 6461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17164-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-17164-2_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17163-5
Online ISBN: 978-3-642-17164-2
eBook Packages: Computer ScienceComputer Science (R0)