QQ客服 官方微博 反馈留言

	Trace-based temporal verification for message-passing programs
	Lei, Jinjiang ; Qiu, Zongyan ; Shao, Zhong
	2014
英文摘要	Verification of concurrent systems is difficult because of their inherent nondeterminism. Modern verification requires clean specifications of inter-thread interferences and modular reasoning over separated components. But for message-passing models, a general reasoning system, which meets these standards, is still in demand. Here we propose a new logic for verifying distributed programs modularly. We concretize the concept of event traces to represent interactions among distributed agents, and constrain the environmental interferences by logical invariants. The verification is compositional w.r.t. agents as long as some inter-agent constraints are satisfied. Using this logic we successfully verified two classic message-passing algorithms: leader election and merging network. Copyright ? 2014 by The Institute of Electrical and Electronics Engineers, Inc.; EI; 0
语种	英语
出处	EI
内容类型	其他
源URL	[http://hdl.handle.net/20.500.11897/329403]
专题	数学科学学院
推荐引用方式 GB/T 7714	Lei, Jinjiang,Qiu, Zongyan,Shao, Zhong. Trace-based temporal verification for message-passing programs. 2014-01-01.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

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