| Title: | assumption generation for asynchronous systems by abstraction refinement |
| Author: | Yang Qiusong
; Clarke Edmund M.
; Komuravelli Anvesh
; Li Mingshu
|
| Source: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|
| Conference Name: | 9th International Symposium on Formal Aspects of Component Software, FACS 2012
|
| Conference Date: | September 12, 2012 - September 14, 2012
|
| Issued Date: | 2013
|
| Conference Place: | Mountain View, CA, United states
|
| Keyword: | Learning algorithms
; Model checking
|
| 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
|
| 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. |
| 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. |
| Language: | 英语
|
| Content Type: | 会议论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/15900
|
| Appears in Collections: | 软件所图书馆_会议论文
|
|
There are no files associated with this item.
|
| Recommended Citation: | |
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.
|
|
|
