QQ客服 官方微博 反馈留言

	Super-dense computation in verification of hybrid CSP processes
	Guelev, Dimitar P. (1) ; Wang, Shuling (2) ; Zhan, Naijun (2) ; Zhou, Chaochen (2)
	2014
会议名称	10th International Symposium on Formal Aspects of Component Software, FACS 2013
会议日期	October 27, 2013 - October 29, 2013
会议地点	Nanchang, China
关键词	Hybrid system Differential invariant Hybrid CSP Duration Calculus Super-dense computation Hybrid Hoare logic
页码	13-22
通讯作者	Wang, S.(wangsl@ios.ac.cn)
中文摘要	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.
收录类别	CPCI ; EI
会议录出版地	Springer Verlag
语种	英语
ISSN号	3029743
ISBN号	9783319076010
内容类型	会议论文
源URL	[http://ir.iscas.ac.cn/handle/311060/16514]
专题	软件研究所_软件所图书馆_会议论文
推荐引用方式 GB/T 7714	Guelev, Dimitar P. ,Wang, Shuling ,Zhan, Naijun ,et al. Super-dense computation in verification of hybrid CSP processes[C]. 见:10th International Symposium on Formal Aspects of Component Software, FACS 2013. Nanchang, China. October 27, 2013 - October 29, 2013.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。