面向移动云服务系统的形式化语义描述方法  

Formal semantic model for mobile cloud service system

作　　者：侯金奎[1] 张玉艳[1] 

机构地区：[1]潍坊学院计算机工程学院,山东潍坊261061

出　　处：《计算机应用研究》2016年第2期467-472,共6页Application Research of Computers

基　　金：山东省优秀中青年科学家科研奖励基金计划资助项目(BS2011DX039);山东省科技发展计划资助项目(2011YD01042;2011YD01043);山东省高等学校优秀中青年骨干教师国际合作培养计划资助项目(2013)

摘　　要：针对移动云服务系统构建过程中架构设计和语义描述等方面存在的问题,以类型范畴理论为基础,为基于agent的移动云服务系统建立了一种形式化语义描述模型。该方法中,将agent描述为范畴理论中的对象节点,agent之间的交互和依赖关系作为态射,将整个云服务系统描述为一个类型范畴图表。在此基础上,对agent交互与协作、架构设计与精化、agent迁移、agent可替代性以及应用请求的可满足性等进行了分析和讨论。该形式化模型增强了系统架构的语义描述能力,有助于对移动云服务系统的规约进行分析和验证。In order to resolve the problems of architecture design and semantic verification of the development process for mo- bile cloud service system, this paper proposed a semantic model for agent-based mobile cloud service system on the basis of typed category theory. It used agent as categorical object, and depicted the interaction and dependencies between agents as mor- phism. Thus it described the whole cloud service system as a typed category diagram. On this basis, this paper undertook a fur- ther analysis and discussion to study about agent interaction and collaboration, architecture design and refinement, agent migra- tion, agent substitutability as well as application request satisfiability. The formal model enhances semantic description capabili- ties of system architecture, and can make an effective support for the analysis and verification of specifications of mobile cloud service systems.

关 键 词：移动云服务 AGENT 形式化描述 语义验证 范畴理论 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]