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

Projection Temporal Logic Oriented Model Checking for Web Services

作　　者：王小兵[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算理论与技术研究所

出　　处：《西安交通大学学报》2009年第4期39-43,124,共6页Journal of Xi'an Jiaotong University

基　　金：国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713)

摘　　要：为了满足Web服务的可靠性,利用投影时序逻辑的模型检测方法来验证Web服务.利用投影时序逻辑的一个可执行子集对OWL-S进行建模,用命题投影时序逻辑来描述期望的性质.模型M和性质P统一以投影时序逻辑来表示,通过判定M蕴含P的有效性,即判定M和非P的合取的不可满足性,亦利用M和非P的正则形可构造合取式的正则图,判定合取的不可满足性,从而达到模型检测的目的.通过运行实例表明,所提模型检测器可验证Web服务系统性质,保证Web服务的可靠性.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.

关 键 词：形式逻辑 投影时序逻辑 WEB服务 模型检测 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]