ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS

ISCAS OpenIR

	ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS
	Lomuscio, Alessio; Strulo, Ben; Walker, Nigel; Wu, Peng
	2013
发表期刊	INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE
ISSN	0129-0541
卷号	24 期号:4 页码:419-444
摘要	We investigate assume-guarantee reasoning for global specifications consisting of conjunctions of local specifications. We present a sound and complete assume-guarantee methodology that enables us to establish properties of a composite system by checking local specifications of its individual modules. We illustrate our approach with an example from the field of network congestion control, where different agents are responsible for controlling packet flow across a shared infrastructure. In this context we derive an assume-guarantee system for network stability and show its efficiency to reason about any number of agents, any initial flow configuration, and any topology of bounded degree.; We investigate assume-guarantee reasoning for global specifications consisting of conjunctions of local specifications. We present a sound and complete assume-guarantee methodology that enables us to establish properties of a composite system by checking local specifications of its individual modules. We illustrate our approach with an example from the field of network congestion control, where different agents are responsible for controlling packet flow across a shared infrastructure. In this context we derive an assume-guarantee system for network stability and show its efficiency to reason about any number of agents, any initial flow configuration, and any topology of bounded degree.
收录类别	SCI
关键词	Assume-guarantee Reasoning Compositional Model Checking Distributed System
部门归属	[Lomuscio, Alessio] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London SW7 2AZ, England. [Strulo, Ben; Walker, Nigel] BT Innovate, Ipswich IP5 7RE, Suffolk, England. [Wu, Peng] Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing 100190, Peoples R China.
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16927
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Lomuscio, Alessio,Strulo, Ben,Walker, Nigel,et al. ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS[J]. INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE,2013,24(4):419-444.
APA	Lomuscio, Alessio,Strulo, Ben,Walker, Nigel,&Wu, Peng.(2013).ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS.INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE,24(4),419-444.
MLA	Lomuscio, Alessio,et al."ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS".INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE 24.4(2013):419-444.