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