中文摘要：

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

英文摘要：

Targeting the problem of weak time awareness, low service utilization and poor composition reliability in the process of web services composition, we propose to bring quantitative timed properties into web services interaction adaptation frame- work and make efforts on researching on time-aware web services interaction modeling, automated interaction mismatch detection and automated adaptor protocol generation. First, we propose timed service protocol （TSP） model to represent interaction behavior of single time-aware web service and timed service protocol network （TSPN） model to represent concurrent composition of multiple time-aware web services; Second, we transform the interaction mismatch detection problem into the determination problem of com- patibility of TSP models,define the mapping rules from time-aware web service descriptions to TSP models and from TSP models to UPPAAL specifications, give the CTL representations of compatibility properties and implement automatically interaction mismatch detection of time-aware web services based on model checker UPPAAL, whose result determines whether it is necessary to build adaptor for the next step. Finally, experiments demonstrate feasibility and validity of above idea.