摘要：针对现有Web服务组合过程中存在时间感知力弱、服务利用率低、组合可靠性差等问题,通过将定量时间属性引入Web服务交互适配框架中,研究时间感知Web服务交互行为的形式化建模与交互行为失配的自动检测问题.提出了用于表达单个时间感知Web服务交互行为的时间服务协议（TSP）模型和用于表达多个时间感知Web服务并发组合的时间服务协议网络（TSPN）模型;将时间感知Web服务交互失配检测问题转化为TSP模型之间的兼容性判定问题,定义了从时间感知Web服务描述至TSP模型和从TSP模型至UPPAAL规约的映射规则,给出了TSP模型兼容性性质的CTL公式表示,基于模型检测工具UPPAAL实现时间感知Web服务交互失配的自动化检测,其检测结果作为下一步是否需要构造适配器的判断依据;最后通过实例分析进一步阐述了上述方法的可行性和有效性.

关键词：时间感知web服务 时间服务协议 时间服务交互 模型检测 失配检测 

单位：苏州大学计算机科学与技术学院; 江苏苏州215006; 中国科学院计算机科学国家重点实验室; 北京100190; 暨南大学深圳旅游学院; 广东深圳518053