QQ客服 官方微博 反馈留言

	Modeling and verification of component connectors in Coq
	Li, Yi ; Sun, Meng
	2015
关键词	Coordination Reo Connector Coq Verification COORDINATION CHECKING REO QOS
英文摘要	Connectors have emerged as a powerful concept for composition and coordination of concurrent activities encapsulated as components and services. Compositional coordination languages like Reo, serve as a means to formally specify and implement connectors. They support large-scale distributed applications by allowing construction of complex component connectors out of simpler ones. In this paper, we present a new approach to modeling and verification of Reo connectors via Coq, a proof assistant based on higher-order logic and A.-calculus. Basic notions in Reo, like nodes and channels, are defined by inductive types. By tracing the data streams, we provide a method for simulation of the behavior and output of a given Reo connector. With input constraints specified, connectors' properties can be proved by induction. Furthermore, properties specified in LTL can be verified using a simulation-based model-checking approach. An access control system is investigated to show our approach. (C) 2015 Elsevier B.V. All rights reserved.; National Natural Science Foundation of China [61202069, 61272160]; Research Fund for the Doctoral Program of Higher Education of China [20120001120103]; SCI(E); EI; ARTICLE; liyi_math@pku.edu.cn; sunmeng@math.pku.edu.cn; 285-301; 113
语种	英语
出处	EI ; SCI
出版者	SCIENCE OF COMPUTER PROGRAMMING
内容类型	其他
源URL	[http://hdl.handle.net/20.500.11897/424799]
专题	数学科学学院
推荐引用方式 GB/T 7714	Li, Yi,Sun, Meng. Modeling and verification of component connectors in Coq. 2015-01-01.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

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