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

王小兵; 段振华

您当前的位置：

首页 >

文章列表页 >

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

更新时间：2025-07-09

- 面向投影时序逻辑的Web服务模型检测
- Projection Temporal Logic Oriented Model Checking for Web Services
- 西安交通大学学报 2009年43卷第4期页码：39-43+124
- 作者机构：
  
  西安电子科技大学计算理论与技术研究所,西安,710071
- 作者简介：
- 基金信息：
  
  : 2008-10-22. 作者简介: 王小兵(1979-),男,讲师. 基金项目: 国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713)
- DOI：
  中图分类号： TP393
- 网络首发：2009-04-10，
  
  纸质出版：2009
- 稿件说明：
移动端阅览
王小兵, 段振华. 面向投影时序逻辑的Web服务模型检测[J]. 西安交通大学学报, 2009,43(4):39-43+124.

Projection Temporal Logic Oriented Model Checking for Web Services[J]. 2009, 43(4): 39-43+124.
王小兵, 段振华. 面向投影时序逻辑的Web服务模型检测[J]. 西安交通大学学报, 2009,43(4):39-43+124. DOI：

Projection Temporal Logic Oriented Model Checking for Web Services[J]. 2009, 43(4): 39-43+124. DOI：

摘要

为了满足Web服务的可靠性

利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模

用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示

通过判定M蕴含P的有效性

即判定M和非P的合取的不可满足性

亦利用M和非P的正则形可构造合取式的正则图

判定合取的不可满足性

从而达到模型检测的目的.通过运行实例表明

所提模型检测器可验证Web服务系统性质

保证Web服务的可靠性.

Abstract

To satisfy the reliability of web services

a model checking approach with the projection temporal logic(PTL)is adopted to verify web services. An executable subset of PTL is used to model OWL-S

and the propositional projection temporal logic(PPTL)is selected to describe desired properties. The model M and property P are both presented in PTL

then the aim of model checking is obtained by determining the validity of M implies P

namely

the unsatisfiability of the conjunction of M and not P

and the unsatisfiability of the conjunction is checked by constructing its normal form graph with the help of the normal forms of M and not P. Executing the example

it shows that the presented model checker can be used to verify the system properties and hence to ensure the reliability of web services.

关键词

Keywords

references

雷丽晖,段振华.基于扩展投影时序逻辑的组合Web服务描述与验证[J].西安交通大学学报,2007 41(10): 1155-1159.

LEI Lihui, DUAN Zhenhua. Specification and verification of composite web services based on extended projection temporal logic [J]. Journal of Xi'an Jiaotong University, 2007, 41(10): 1155-1150.

ANKOLEKAR A, PAOLUCCI M, SYCARA K. Towards a formal verification of OWL-S process models [C]∥Proceedings of LISWC 2005. Berlin, Germany: Springer-Verlag, 2005: 37-51.

MOSZKOWSKI B C. Executing temporal logic programs[M]. Cambridge, UK: Cambridge University Press, 1986.

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

唐稚松.时序逻辑程序设计与软件工程[M].北京:科学出版社,1999.

NARAYANAN S, MCSHEILA A. Simulation, verification and automated composition of web services [C]∥Proceedings of the 11th International Conference on World Wide Web. New York, NY, USA: ACM, 2002: 77-88.

侯丽珊,金芝,吴步丹.需求驱动的Web服务建模及其验证; 一个基于本体的方法[J].中国科学; E辑,2006 36(10): 1189-1219.

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.

浏览量

下载量

CSCD

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

提交

工具集

关联资源

一种基于最小覆盖的复杂Web 服务组合方法

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

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

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

基于扩展投影时序逻辑的组合Web服务描述与验证