An Assume/Guarantee Based Compositional Calculus for Hybrid CSP

摘要

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 coinpositionally by using assume/guarantee reasoning.