| assume-guarantee reasoning with local specifications | |
| Lomuscio Alessio; Strulo Ben; Walker Nigel; Wu Peng | |
| 2010 | |
| 会议名称 | 12th International Conference on Formal Engineering Methods, ICFEM 2010 |
| 会议录名称 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| 页码 | 204-219 |
| 会议日期 | 40848 |
| 会议地点 | Shanghai, China |
| 收录类别 | EI |
| 出版地 | Germany |
| ISSN | 3029743 |
| ISBN | 3642169007 |
| 部门归属 | (1) Department of Computing, Imperial College London, United Kingdom; (2) BT Innovate, Adastral Park, United Kingdom; (3) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China |
| 摘要 | We investigate assume-guarantee reasoning for global specifications consisting of conjunctions of local specifications. We present a sound and complete assume-guarantee rule that permits reasoning about individual modules for local specifications and draws conclusions on global specifications. 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 rule for system stability, and show that this rule is valuable to reason about any number of agents, any initial flow configuration, and any topology of bounded degree. © 2010 Springer-Verlag Berlin Heidelberg. |
| 关键词 | Specifications System Stability |
| 内容类型 | 会议论文 |
| URI标识 | http://ir.iscas.ac.cn/handle/311060/8668 |
| 专题 | 基础软件与系统重点实验室 |
| 推荐引用方式 GB/T 7714 | Lomuscio Alessio,Strulo Ben,Walker Nigel,et al. assume-guarantee reasoning with local specifications[C]. Germany,2010:204-219. |
| 条目包含的文件 | ||||||
| 文件名称/大小 | 文献类型 | 版本类型 | 开放类型 | 使用许可 | ||
| assume-guarantee rea（256KB） | 开放获取 | -- | 请求全文 | |||
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论