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

杨琛 1; 2; 3; 段振华 1; 2

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-07-09

- PPTL模型检测器实现的一个关键技术
- A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic
- 西安交通大学学报 2010年44卷第10期页码：24-29
- 作者机构：
  
  1. 实验室,西安,710071
  2. 武汉大学软件工程国家重点实验室,武汉,430072
- 作者简介：
- 基金信息：
  
  : 2010-01-20. 作者简介: 杨琛(1981-),男,博士生;段振华(联系人),男,教授,博士生导师. 基金项目: 国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60433010,60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)
- DOI：
  中图分类号： TP393
- 网络首发：2010-10-10，
  
  纸质出版：2010
- 稿件说明：
移动端阅览
杨琛 1, 2, 3, 等. PPTL模型检测器实现的一个关键技术[J]. 西安交通大学学报, 2010,44(10):24-29.

A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic[J]. 2010, 44(10): 24-29.
杨琛 1, 2, 3, 等. PPTL模型检测器实现的一个关键技术[J]. 西安交通大学学报, 2010,44(10):24-29. DOI：

A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic[J]. 2010, 44(10): 24-29. DOI：

摘要

针对命题线性时序逻辑表达能力有限的问题

设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机

将PPTL公式表达的性质转换为性质自动机

通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制

从而改进了验证算法

使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明

该模型检测器可以减少无效验证产生的无效迹数目

有效地实现PPTL模型检测.

Abstract

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 AP.In order to determine whether S satisfies P or not

the product of automata AS and AP 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.

关键词

Keywords

references

MIAO Huaikou, ZENG Hongwei. Model checking-based verification of web application [C]∥ICECCS 2007.Piscataway, NJ, USA: IEEE Computer Society Press,2007: 47-55.

王小兵, 段振华. 面向投影时序逻辑的Web服务模型检测 [J], 西安交通大学学报, 2009, 43(4): 39-44.

WANG Xiaobing, DUAN Zhenhua. Projection temporal logic oriented model checking for web services [J]. Journal of Xi'an Jiaotong University, 2009, 43(4): 39-44.

MEI Jia, MIAO Huaikou, LIU Pan. Applying SMV for security protocol verification [J]. Information Technology Journal, 2009, 8(7):1065-1070.

舒新峰, 段振华. 利用投影时序逻辑的多内核进程调度建模与验证 [J], 西安交通大学学报, 2010, 44(3): 52-57.

SHU Xinfeng; DUAN Zhenhua. Modeling and verification of processes scheduling based on projection temporal logic for multi core CPU [J]. Journal of Xi'an Jiaotong University, 2010, 44(3): 52-57.

HOLZMANN G J. The SPIN model checker: primer and reference manual [M]. Reading, Massachusetts, USA: Addison-Wesley, 2003.

LICHTENSTEIN O, PNUELI A. Checking that finite state concurrent programs satisfy their linear specification [C]// Proceedings of the 12th Annual ACM Symposium on Principles of Programming Languages.New York, USA: ACM Press, 1985: 97-107.

DUAN Zhenhua, TIAN Cong, ZHANG Li. A decision procedure for propositional projection temporal logic with infinite models [J]. Acta Informatica, 2008, 45(1): 43-78.

TIAN Cong, DUAN Zhenhua. Propositional projection temporal logic, Büchi automata and omega-regular expressions [C]//Proceedings of TAMC'08. Berlin, Germany: Springer, 2008: 47-58.

DUAN Zhenhua, YANG Xiaoxiao, KOUTNY M. Framed temporal logic programming [J]. Science of Computer Programming, 2008, 70(1): 31-61.

段振华,杨琛,张笑星,等. 命题投影时序逻辑模型检测器 [EB/OL]. [2010-01-01].http://www.keepandshare.com/doc/view.php?id=1676421da=y.

SCHNEIDER F B. Decomposing properties into safety and liveness using predicate logic, TR 87-874 [R]. Ithaca, NY, USA: Cornell University. Computer Science Department, 1987.

杨琛,张笑星.衡量SPIN性能的基准实例 [EB/OL]. [2010-01-01].http://www.keepandshare.com/doc/view.php?id=1.

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

面向命题投影时序逻辑的安全协议模型检测

应用UML2.0模型的测试用例生成方法

面向投影时序逻辑的Web服务模型检测

结构-语义-残差协同的图像压缩框架：面向隐私保护与高保真重建

电子级超纯氮深冷空分流程节能优化研究