移动计算环境下服务不确定性的语义建模与镇定

At present, it is a great challenge to improve the stability of service availability, reliability and performance in the service-oriented mobile computing. So, basing on my previous research: the uncertainty model of service in mobile computing and aiming at the inadequacy of this model in the expression and verification of service dynamic semantics, this project focuses on the change of service status and the characteristics of interactive behavior in the mobile computing environment to develop the Martin-L?f type theory so that it can both describe service interactive behavior and verify service dynamic semantics. On the theoretical basis of the developed Martin-L?f type theory and Bayesian networks, this project establishes a semantic model and linguistic description of service uncertainty in the mobile computing environment to achieve formal description of service uncertainty. Furthermore, the theory and the mechanism of semantic verification based on the developed Martin-L?f type theory are improved in this research. According to the obtained reasoning technology and the achievement that our study group has made, this project further focuses on the strategies of reducing or removing service uncertainty, the alert mechanism of service uncertainty, and the mechanism of service behavior coordination and scheduling,and they is yet validated and applied via mobile e-pay service. The realization of this project has important theoretical significance and great value of practical application to the mobile enabled cloud service.

提高服务可用、可靠及性能等方面的稳定性是当前移动服务计算中急待解决的挑战性问题。本项目以前期研究成果- - 移动计算中服务不确定性模型为基础，针对该模型对服务动态语义表达和验证的不足，结合移动计算环境下服务状态变迁和交互行为的特点，拓展直觉类型论，使其能兼顾服务交互行为描述和动态语义验证两方面的效能，并以拓展的直觉类型论、贝叶斯网络和本体为基础理论工具，建立移动计算环境下服务不确定性语义模型和服务不确定性描述语言，实现服务不确定性的语义形式化描述。以此为基础，完善基于拓展直觉类型论的语义验证理论与机制，并结合已有推理技术和研究团队已取得的平台基础，建立移动计算环境下降低或者消除服务不确定性的策略、服务不确定性预警机制、服务（含相关资源）行为协调与调度机制（含实现算法），并基于移动电子支付服务进行验证与示范。项目的实施对可移动云服务发展具有重要理论意义和实际应用价值。

提高服务可用、可靠及性能等方面的稳定性是当前移动服务计算中急待解决的挑战性问题。本项目主要研究移动计算环境下服务不确定的语义建模与镇定技术，主要研究成果如下。.1.针对现有方法对服务动态语义表达和验证的不足，研究移动计算环境下服务状态变迁和交互行为逻辑，基于行为类型拓展了Martin-Löf’s类型论，实现服务交互行为描述和动态语义验证。.2.根据宿居上下文因素或独立因素，通过形式化方法构建移动环境下服务概率模型，实现统一服务不确定性语义模型建模。.3.完善基于消息语义的服务验证理论与机制，建立面向移动计算的服务不确定性描述语言规范，提出基于拓展类型论的服务描述语言。.4.研究服务不确定性理论，解决移动计算环境下服务及其不确定性的语义验证问题，结合已取得的平台基础，建立移动计算环境下降低或者消除服务不确定性的策略、服务不确定性预警机制、服务行为协调与调度机制，提出了以数据保障、服务替换为代表的辅助方法，实现移动服务的不确定性验证与镇定。.项目以服务建模为中心完善了不确定性基础理论，并已从语义模型、描述语言及语义验证、不确定性镇定等方面展开研究，在移动支付、资源存储、健康管理等方面对移动服务进行验证与示范，取得了较好的研究成果。项目的实施对可移动云服务发展具有重要理论意义和实际应用价值。