assumption generation for asynchronous systems by abstraction refinement

ISCAS OpenIR

	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
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	260-276
会议日期	September 12, 2012 - September 14, 2012
会议地点	Mountain View, CA, United states
收录类别	EI
ISSN	0302-9743
ISBN	9783642358609
部门归属	(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
摘要	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.
关键词	Learning Algorithms Model Checking
语种	英语
内容类型	会议论文
URI标识	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],2013:260-276.