an assume/guarantee based compositional calculus for hybrid csp

ISCAS OpenIR

	an assume/guarantee based compositional calculus for hybrid csp
	Wang Shuling; Zhan Naijun; Guelev Dimitar
	2012
会议名称	9th Annual Conference on Theory and Applications of Models of Computation, TAMC 2012
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	72-83
会议日期	May 16, 2012 - May 21, 2012
会议地点	Beijing, China
收录类别	EI
ISSN	0302-9743
ISBN	9783642299513
部门归属	(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
摘要	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.
关键词	Differential Equations Hybrid Systems
主办者	State Key Laboratory of Computer Science; Chinese Academy of Sciences, Institute of Software; Chinese Academy of Sciences
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15723
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Wang Shuling,Zhan Naijun,Guelev Dimitar. an assume/guarantee based compositional calculus for hybrid csp[C],2012:72-83.