Institutional Repository
| an assume/guarantee based compositional calculus for hybrid csp | |
| Wang Shuling; Zhan Naijun; Guelev Dimitar | |
| 2012 | |
| Conference Name | 9th Annual Conference on Theory and Applications of Models of Computation, TAMC 2012 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 72-83 |
| Conference Date | May 16, 2012 - May 21, 2012 |
| Conference Place | Beijing, China |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642299513 |
| Department | (1) State Key Lab. of Comput. Sci. Institute of Software Chinese Academy of Sciences China; (2) Institute of Mathematics and Informatics Bulgarian Academy of Sciences Bulgaria |
| English Abstract | 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.; 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. |
| Keyword | Differential Equations Hybrid Systems |
| Sponsorship | State Key Laboratory of Computer Science; Chinese Academy of Sciences, Institute of Software; Chinese Academy of Sciences |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15723 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Wang Shuling,Zhan Naijun,Guelev Dimitar. an assume/guarantee based compositional calculus for hybrid csp[C],2012:72-83. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment