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

作     者：杨琛 段振华 YANG Chen;DUAN Zhenhua

作者机构：西安电子科技大学计算理论与技术研究所西安710071 西安电子科技大学ISN国家重点实验室西安710071 武汉大学软件工程国家重点实验室武汉430072 

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

出 版 物：《西安交通大学学报》 (Journal of Xi'an Jiaotong University)

年 卷 期：2010年第44卷第10期

页      码：24-29页

摘      要：针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.

主 题 词：时序逻辑 自动机 模型检测 

学科分类：0810[工学-土木类] 12[管理学] 1201[管理学-管理科学与工程类] 08[工学] 0805[工学-能源动力学] 081201[081201] 0812[工学-测绘类] 

核心收录：

馆 藏 号：203114192...