Super-dense computation in verification of hybrid CSP processes

ISCAS OpenIR

	Super-dense computation in verification of hybrid CSP processes
	Guelev, Dimitar P. (1); Wang, Shuling (2); Zhan, Naijun (2); Zhou, Chaochen (2); Wang, S.(wangsl@ios.ac.cn)
	2014
会议名称	10th International Symposium on Formal Aspects of Component Software, FACS 2013
页码	13-22
会议日期	October 27, 2013 - October 29, 2013
会议地点	Nanchang, China
收录类别	CPCI ; EI
出版地	Springer Verlag
ISSN	3029743
ISBN	9783319076010
部门归属	(1) Institute of Mathematics and Informatics, Bulgarian Academy of Sciences, Sofia, Bulgaria; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
摘要	Hybrid Communicating Sequential Processes (HCSP) extends CSP to include differential equations and interruptions. We feel comfortable in our experience with HCSP to model scenarios of the Level 3 of Chinese Train Control System (CTCS-3), and to define a formal semantics for Simulink. The Hoare style calculus of [5] proposes a calculus to verify HCSP processes. However it has an error with respect to super-dense computation. This paper is to establish another calculus for a subset of HCSP, which uses Duration Calculus formulas to record program history, negligible time state to denote super-dense computation and semantic continuation to avoid infinite interval. It is compositional and sound. © 2014 Springer International Publishing Switzerland.; Hybrid Communicating Sequential Processes (HCSP) extends CSP to include differential equations and interruptions. We feel comfortable in our experience with HCSP to model scenarios of the Level 3 of Chinese Train Control System (CTCS-3), and to define a formal semantics for Simulink. The Hoare style calculus of [5] proposes a calculus to verify HCSP processes. However it has an error with respect to super-dense computation. This paper is to establish another calculus for a subset of HCSP, which uses Duration Calculus formulas to record program history, negligible time state to denote super-dense computation and semantic continuation to avoid infinite interval. It is compositional and sound. © 2014 Springer International Publishing Switzerland.
关键词	Hybrid System Differential Invariant Hybrid Csp Duration Calculus Super-dense Computation Hybrid Hoare Logic
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16514
专题	中国科学院软件研究所
通讯作者	Wang, S.(wangsl@ios.ac.cn)
推荐引用方式 GB/T 7714	Guelev, Dimitar P. ,Wang, Shuling ,Zhan, Naijun ,et al. Super-dense computation in verification of hybrid CSP processes[C]. Springer Verlag,2014:13-22.