assumption generation for asynchronous systems by abstraction refinement
文献类型：会议论文
| 作者 | Yang Qiusong ; Clarke Edmund M. ; Komuravelli Anvesh ; Li Mingshu |
| 出版日期 | 2013 |
| 会议名称 | 9th International Symposium on Formal Aspects of Component Software, FACS 2012 |
| 会议日期 | September 12, 2012 - September 14, 2012 |
| 会议地点 | Mountain View, CA, United states |
| 关键词 | Learning algorithms Model checking |
| 页码 | 260-276 |
| 中文摘要 | Compositional verification provides a way for deducing properties of a complete program from properties of its constituents. In particular, the assume-guarantee style of reasoning splits a specification into assumptions and guarantees according to a given inference rule and the generation of assumptions through machine learning makes the automatic reasoning possible. However, existing works are purely focused on the synchronous parallel composition of Labeled Transition Systems (LTSs) or Kripke Structures, while it is more natural to model real software programs in the asynchronous framework. In this paper, shared variable structures are used as system models and asynchronous parallel composition of shared variable structures is defined. Based on a new simulation relation introduced in this paper, we prove that an inference rule, which has been widely used in the literature, holds for asynchronous systems as long as the components' alphabets satisfy certain conditions. Then, an automating assumption generation approach is proposed based on counterexample-guided abstraction refinement, rather than using learning algorithms. Experimental results are provided to demonstrate the effectiveness of the proposed approach. © 2013 Springer-Verlag. |
| 英文摘要 | Compositional verification provides a way for deducing properties of a complete program from properties of its constituents. In particular, the assume-guarantee style of reasoning splits a specification into assumptions and guarantees according to a given inference rule and the generation of assumptions through machine learning makes the automatic reasoning possible. However, existing works are purely focused on the synchronous parallel composition of Labeled Transition Systems (LTSs) or Kripke Structures, while it is more natural to model real software programs in the asynchronous framework. In this paper, shared variable structures are used as system models and asynchronous parallel composition of shared variable structures is defined. Based on a new simulation relation introduced in this paper, we prove that an inference rule, which has been widely used in the literature, holds for asynchronous systems as long as the components' alphabets satisfy certain conditions. Then, an automating assumption generation approach is proposed based on counterexample-guided abstraction refinement, rather than using learning algorithms. Experimental results are provided to demonstrate the effectiveness of the proposed approach. © 2013 Springer-Verlag. |
| 收录类别 | EI |
| 会议录 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
 |
| 语种 | 英语 |
| ISSN号 | 0302-9743 |
| ISBN号 | 9783642358609 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/15900]  |
| 专题 | 软件研究所_软件所图书馆_会议论文 |
| 推荐引用方式 GB/T 7714 | Yang Qiusong,Clarke Edmund M.,Komuravelli Anvesh,et al. assumption generation for asynchronous systems by abstraction refinement[C]. 见:9th International Symposium on Formal Aspects of Component Software, FACS 2012. Mountain View, CA, United states. September 12, 2012 - September 14, 2012. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。