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

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

项目编号： No.60970010

项目类型： 面上项目

立项/批准年度： 2010

项目学科： 自动化技术、计算机技术

项目作者： 黄林鹏

作者单位： 上海交通大学

项目金额： 30万元

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

中文关键词： 服务组合；可信计算；普适计算；；

英文摘要：

英文关键词： service composition；trustworthiness computing；pervasive computing；；