Symbolic model checking APSL

作     者：Wanwei LIU Ji WANG Huowang CHEN Xiaodong MA Zhaofei WANG 

作者机构：National Laboratory for Par'diet and Distributed Processing School of ComputerNational University of Defense Technology Changsha 410073 China 

出 版 物：《中国高等学校学术文摘·计算机科学》 (FRONTIERS OF COMPUTER SCIENCE IN CHINA)

年 卷 期：2009年第3卷第1期

页      面：130-141页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：Hunan Natural Science Foundation, (07331011) National High-Tech Research and Development Plan of China, (2006AA01Z429) National Natural Science Foundation of China, NSFC, (60673118, 60725206, 90612009) 

主　　题：property specification language symbolic model checking tableau approach extended NuSMV 

摘      要：Property specification language (PSL) is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. In this paper, we present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be easily implemented via the BDD based symbolic approach. Moreover, we implement an extension of NuSMV, and this adapted version supports symbolic model checking of APSL. Experimental results show that this variant of PSL can be efficiently verified. Henceforth, symbolic model checking PSL can be carried out by a transformation from PSL to APSL and symbolic model checking APSL.