普适计算中可信服务构建的形式化分析与验证

普适计算通常是在一个异构、移动、开放的环境下进行，不仅需要考虑系统内部各个组件之间的协调合作还要关注系统与外部环境的交互，传统的服务计算理论和技术很难直接有效应用。本项目拟针对普适环境下服务计算的可信保障问题，提出一种描述普适环境下服务特征的形式化语言，给出面向普适应用的类型和效果系统以刻画和抽取构建的普适服务的动态行为，并把它们转换为服务流程有限状态机；设计基于抽象状态机的服务行为验证模型，根据上述服务流程有限状态机和用户给定的规约策略，自动验证服务的动态运行行为是否符合用户所给定的规约策略和相关的性质，并推导出服务行为的失效点与可恢复点的映射转换机制，为移动环境下普适服务的快速重建提供理论指导并避免传统基于有限状态机分析中可能出现的状态爆炸问题；最后基于OSGi构建普适应用场景，对提出的理论模型和技术方案进行验证。

本项目以普适环境下的可信服务构建为研究对象，以建立符合用户规约和行为策略的服务编排模型为目标，使用形式化分析和验证方法确保普适环境下服务计算的可信性，搭建基于OSGi 的普适计算平台和应用场景以验证课题组提出的理论和方法的可行性和有效性，取得成果如下：.（1）普适环境下服务构件特征的建模研究.普适环境下计算的复杂性和可变性使普适服务的构件特征和传统服务的构件特征相比有较大的不同，因而需要对普适服务构件的特征进行建模，课题组研究了普适环境下服务构件的主要特性，包括普适服务接口类型、服务行为表达、服务行为规约策略和服务感知接口等，分析了普适计算环境下服务构件的交互方式和组合模式，提出了一种面向普适环境的服务模型，其具有较好的自适应性并可支持动态演化。.（2）基于类型和效果系统的服务编排形式化分析.普适环境下服务具有的动态特征使服务编排更为复杂，系统不仅需要关注服务的运行行为是否与用户的规约一致，而且要求服务遵循一些指定的策略，如服务行为一致、资源使用保护等。课题组将类型和效果系统静态分析技术应用到普适服务编排计划，形式化分析了普适服务编排计划的可信性。研究工作包括基于类型和效果系统的服务编排建模技术，服务发布、服务发现、服务调用、服务编排和流程计划的形式化描述；项目组给出了基于行为一致的服务替换方法，并推导了类型安全性定理，设计了服务替换分析工具，提出了一种面向普适环境的服务重建方法。.（3）基于抽象状态机的分析与验证模型.项目组设计了服务执行分析抽象状态机，根据一致性要求及行为策略定义分析服务流程，从而得到服务协作执行中可能的失效点，并设计失效点与服务执行恢复状态点的映射转换机制，从而实现服务动态进入和退出的透明性；设计行为策略及一致性验证抽象状态机，通过该抽象状态机的模拟执行，自动验证服务行为的一致性以及验证候选服务是否违背行为策略。.（4）构建可验证的普适环境下的服务计算平台.基于OSGi 搭建一个普适计算平台并构建典型的普适应用场景，对上述理论和方法进行验证；通过将抽象状态机的执行引擎、类型和效果系统的分析工具以及服务流程向有限状态机的转换工具整合到上述普适服务计算平台中，构建了一个可信普适应用开发原型。