Bounded Model Checking of ACTL formulae

摘要：

In this paper, we give a new and improved Bounded Model Checking encoding method for the universal frag ment of CTL (ACTL). More specifically, the new encoding method works for verification of ACTL properties, instead of error-hunting. Combine our verification encoding and bug-hunting encoding proposed before, we get a Bounded Model Checking procedure that works for both valid and invalid ACTL properties. The underlying idea and intuition are summarized in this paper and we implement our tool BMV (Bounded Model Verification) on top of the well known model checker NuSMV 2, and conduct experiments that show the strength and weakness of ACTL Bounded Model Checking compared to traditional BDD-based model checking procedure.

作者: Wei Chen Wenhui Zhang

作者单位: Institute of Software, Chinese Academy of Sciences Beijing, China Graduate University of Chinese Aca Institute of Software Chinese Academy of Sciences Beijing, China

会议类型: 国际会议

会议名称: Third International Symposium on Theoretical Aspects of Software Engineering TASE 2009(第三届软件工程理论国际研讨会)

会议地点: 天津

会议语种:英文

页码: 90-99

在线出版日期: 2009-07-29（万方平台首次上网日期，不代表论文的发表时间）