Institutional Repository
| assumption generation for asynchronous systems by abstraction refinement | |
| Yang Qiusong; Clarke Edmund M.; Komuravelli Anvesh; Li Mingshu | |
| 2013 | |
| Conference Name | 9th International Symposium on Formal Aspects of Component Software, FACS 2012 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 260-276 |
| Conference Date | September 12, 2012 - September 14, 2012 |
| Conference Place | Mountain View, CA, United states |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642358609 |
| Department | (1) National Engineering Research Center of Fundamental Software Institute of Software Chinese Academy of Sciences Beijing 100190 China; (2) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China; (3) Computer Science Department Carnegie Mellon University Pittsburgh PA 15213 United States |
| English Abstract | 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. |
| Keyword | Learning Algorithms Model Checking |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15900 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Yang Qiusong,Clarke Edmund M.,Komuravelli Anvesh,et al. assumption generation for asynchronous systems by abstraction refinement[C],2013:260-276. |
| 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