Institutional Repository
| ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS | |
| Lomuscio, Alessio; Strulo, Ben; Walker, Nigel; Wu, Peng | |
| 2013 | |
| Source | INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE
 |
| ISSN | 0129-0541 |
| Volume | 24Issue:4Pages:419-444 |
| English Abstract | 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. |
| Indexed Type | SCI |
| Keyword | Assume-guarantee Reasoning Compositional Model Checking Distributed System |
| Department | [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. |
| Language | 英语 |
| Content Type | 期刊论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/16927 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation 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. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment