A refinement calculus for hybrid systems

ISCAS OpenIR

	A refinement calculus for hybrid systems
	Gu, Bin (1); Zou, Liang (2); Zou, Liang
	2014
会议名称	2014 19th International Conference on Engineering of Complex Computer Systems, ICECCS 2014
页码	176-185
会议日期	August 4, 2014 - August 7, 2014
会议地点	Tianjin, China
收录类别	EI
出版地	Institute of Electrical and Electronics Engineers Inc.
ISBN	9781479954827
部门归属	(1) School of Computer Science, Northwestern Polytechnical University, Beijing, China; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China
摘要	System-level design for hybrid systems is complex and error-prone. To ensure correctness, formal methods are usually considered, and have been successfully applied in practice. Refinement for discrete systems is well-known, while little work has been done for hybrid systems. In this paper, we first present an envelope semantics for hybrid systems, where control and physical devices are separately described. Then, we relate the semantics to hybrid CSP (a well-known compositional modelling language for hybrid systems) by a Galois connection, to show its reasonableness. Based on this, we define a set of refinement rules that refine an abstract specification to a lower-level implementation. In the end, several examples are provided to show our methodology. Moreover, in our methodology classical refinement calculus is reused, and the soundness is provided by a monotonicity law.; System-level design for hybrid systems is complex and error-prone. To ensure correctness, formal methods are usually considered, and have been successfully applied in practice. Refinement for discrete systems is well-known, while little work has been done for hybrid systems. In this paper, we first present an envelope semantics for hybrid systems, where control and physical devices are separately described. Then, we relate the semantics to hybrid CSP (a well-known compositional modelling language for hybrid systems) by a Galois connection, to show its reasonableness. Based on this, we define a set of refinement rules that refine an abstract specification to a lower-level implementation. In the end, several examples are provided to show our methodology. Moreover, in our methodology classical refinement calculus is reused, and the soundness is provided by a monotonicity law.
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16595
专题	中国科学院软件研究所
通讯作者	Zou, Liang
推荐引用方式 GB/T 7714	Gu, Bin ,Zou, Liang ,Zou, Liang. A refinement calculus for hybrid systems[C]. Institute of Electrical and Electronics Engineers Inc.,2014:176-185.