文献类型：期刊文章

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

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

出　　处：《西安交通大学学报》

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

年　　份：2009

卷　　号：43

期　　号：4

起止页码：39-43

语　　种：中文

收录情况：BDHX、BDHX2008、CAS、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、EI(收录号：20091912076972)、IC、INSPEC、JST、MR、RCCSE、SCOPUS、ZGKJHX、ZMATH、核心刊

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

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

分 类 号：TP393]