Hybrid CSP (HCSP) extends CSP to describe interacting continuous and discrete dynamics. The concurrency with synchronous communications, timing constructs, interrupts, differential equations, and so on, make the behavior of HCSP difficult to specify and verify. In this paper, we propose a Hoare style calculus for reasoning about HCSP. The calculus includes Duration Calculus formulas to record process execution history and reason about real-time properties and continuous evolution, and dedicated predicate symbols to specify communication traces and readiness of process actions so that the composite constructs of HCSP can be handled compositionally by using assume/guarantee reasoning. © 2012 Springer-Verlag.
CITATION STYLE
Wang, S., Zhan, N., & Guelev, D. (2012). An assume/guarantee based compositional calculus for hybrid CSP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7287 LNCS, pp. 72–83). https://doi.org/10.1007/978-3-642-29952-0_13
Mendeley helps you to discover research relevant for your work.