PSL的有界模型检验  

Bounded Model Checking of PSL

作　　者：虞蕾[1,2] 赵宗涛[2] 

机构地区：[1]国防科学技术大学计算机学院博士后流动站,湖南长沙410073 [2]第二炮兵工程学院计算机系,陕西西安710025

出　　处：《电子学报》2009年第3期614-621,共8页Acta Electronica Sinica

基　　金：国家高技术研究发展计划(863计划)课题(No.2007AA010301);国家自然科学基金(No.60503032);中国博士后科学基金(No.20080431401)

摘　　要：基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.SAT-based bounded model checking （BMC） is introduced as a complementary technique to OBDD-based symbolic model checking, and is a verification method for parallel and reactive systems. However, until now the properties verified by bounded model checking are very limited. Temporal logic PSL is a property specification language （IEEE-1850） describing parallel systems and is divided into two parts,i.e.the linear time logic FL（Foundation Language）and the branch time logic OBE（Optional Branching Extension）. The specification checked by BMC is extended to PSL and its algorithm is also proposed. Firstly, define the bounded semantics of PSL,and then reduce the bounded semantics into SAT by translating PSL specification formula and the state transition relation of the system M into the propositional formulas, respectively. Finally, verify the satisfiability of the conjunction of the two propositional formulas. The algorithm results in the translation of the existential model checking of the temporal logic PSL into the satisfiability problem of propositional formula. An example of a queue controlling circuit is used to interpret detailedly the executing procedure of the algorithm.

关 键 词：PSL(property specification language) 有界模型检验(bounded model checking BMC) SAT(propositional satisfiability) OBDD(ordered binary decision diagram) 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]