中国科学院机构知识库网格
Chinese Academy of Sciences Institutional Repositories Grid
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
其他版本

除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。