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

被引：7

作者：

王小兵

段振华

机构：

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

来源：

西安交通大学学报 | 2009年 / 04期

关键词：

形式逻辑; 投影时序逻辑; Web服务; 模型检测;

D O I：

暂无

中图分类号：

TP311.52 [];

学科分类号：

081202 ; 0835 ;

摘要：

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

引用

页码：39 / 43+124 +124

页数：6

共 4 条

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