| PPTL模型检测器实现的一个关键技术 |
| |
| 引用本文： | 杨琛,段振华.PPTL模型检测器实现的一个关键技术[J].西安交通大学学报,2010,44(10). |
| |
| 作者姓名： | 杨琛 段振华 |
| |
| 作者单位： | 1. 西安电子科技大学计算理论与技术研究所,710071,西安;西安电子科技大学ISN国家重点实验室,710071,西安;武汉大学软件工程国家重点实验室,430072,武汉
2. 西安电子科技大学计算理论与技术研究所,710071,西安;西安电子科技大学ISN国家重点实验室,710071,西安 |
| |
| 基金项目： | 国家自然科学基金重大国际合作项目，国家自然科学基金资助项目，国家重点基础研究发展规划资助项目，武汉大学软件工程国家重点实验室开放基金资助项目，中央高校基本科研业务费专项资金资助项目 |
| |
| 摘 要： | 针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.
|
| 关 键 词： | 时序逻辑 自动机 模型检测 |
A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic |
| |
| YANG Chen,DUAN Zhenhua.A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic[J].Journal of Xi'an Jiaotong University,2010,44(10). |
| |
| Authors: | YANG Chen DUAN Zhenhua |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
