Projection Temporal Logic Oriented Model Checking for Web Services

您当前的位置：

首页 >

文章列表页 >

Projection Temporal Logic Oriented Model Checking for Web Services

更新时间：2025-07-09

- Projection Temporal Logic Oriented Model Checking for Web Services
- Vol. 43, Issue 4, Pages: 39-43+124(2009)
- 作者机构：
  
  西安电子科技大学计算理论与技术研究所,西安,710071
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP393
- Online First：10 April 2009，
  
  Published：2009
- 稿件说明：
移动端阅览
Projection Temporal Logic Oriented Model Checking for Web Services[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.

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Minimum Coverage Method for Complicated Web Service Composition

Model-Checking Security Protocol with Propositional Projection Temporal Logic

A Key Technique to Develop the Model Checker for Propositional Projection Temporal Logic

Test Case Generation Based on UML2.0 Models

Specification and Verification of Composite Web Services Based on Extended Projection Temporal Logic

Related Author

李增智 1

胡亚红 2

伍卫国 1

朱正东 1

王小兵 1

段振华 1

Related Institution

Department of Computer Science and Technology, Xi'an Jiaotong University

State Key Laboratory of Software Engineering, Wuhan University

实验室

武汉大学软件工程国家重点实验室

State Key Laboratory of Integrated Service Networks, Xidian University

⁰