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

摘要：

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

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

所属期刊栏目：44

分类号：TP393(计算技术、计算机技术)

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

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

页数：共6页

页码：24-29