assumption generation for asynchronous systems by abstraction refinement

CORC > 软件研究所 > 软件所图书馆 > 会议论文

	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.