PPTL模型检测器实现的一个关键技术  

A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic

作　　者：杨琛[1,2,3] 段振华[1,2] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071 [2]西安电子科技大学ISN国家重点实验室,西安710071 [3]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《西安交通大学学报》2010年第10期24-29,共6页Journal of Xi'an Jiaotong University

基　　金：国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60433010;60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)

摘　　要：针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.The propositional projection temporal logic（PPTL）has more expressive power than other linear temporal logics,for example,the propositional linear-time temporal logic（PLTL）,and thus is more suitable for use as a specification language in model checking.Hence,a key technique for PPTL model checker is presented.The model checker interprets a ProMeLa model S as a Büchi automaton AS,and transforms PPTL property P to an automaton A P.In order to determine whether S satisfies P or not,the product of automata AS and A P is computed and it is checked whether the product automaton accepts the empty word or not.The checking algorithm is implemented based on SPIN.However,since PPTL contains both finite and infinite models,SPIN cannot be used off-the-shelf.To cope with the problem,the related algorithm in SPIN is modified to support PPTL.Experimental results show that the PPTL model checker can effectively perform model checking against PPTL properties.

关 键 词：时序逻辑 自动机 模型检测 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]