一种改进的安全环境演算及其行为等价关系研究  

Variant of Safe Ambient Calculus and its Contextual Bisimulation

作　　者：韩婷婷[1] 陈韬略[1] 吕建[1] 马骞[1] 

机构地区：[1]南京大学计算机软件新技术国家重点实验室,江苏南京210093

出　　处：《小型微型计算机系统》2005年第6期1037-1041,共5页Journal of Chinese Computer Systems

基　　金：国家重点基础研究发展规划"九七三"项目(2002CB312002)资助;国家自然科学基金(60273034;60233010)资助;国家"八六三"高科技项目(2002AA116010)资助.

摘　　要：移动计算是在网络技术发展过程中涌现出来的一种新的分布计算范型.移动环境演算是一种广为使用的描述移动计算的形式化模型.安全环境演算为每个动作原语增加了一个相应的协动作原语,从而解决了强干扰问题.然而,SA的语法定义在直觉上并不能很好地描述out原语的协动作,同时其代数性质也存在一些缺陷.针对这些问题,一方面调整了SA的归约关系,将出入动作的语义统一在“进入时检查”这一约定之下,使其更符合直觉含义.在此基础上,通过采用Honda-Yoshida的技术,定义开接口互模拟等价关系,修正了SA代数性质上的缺陷,并通过一个防火墙的例子说明了改进的安全环境演算及其行为等价关系的合理性.Computation with mobility becomes a novel distributed computation paradigm with the development of network technology. The calculus of Mobile Ambient is a widely studied formal mechanism for describing both mobile computing and mobile computation. This paper deals with one of its variants, the Safe Ambient calculus (SA) . In details, this paper modify the syntactic definition of SA, as a result, the security checking action is unified to be executed when an ambient is to be entered, which makes it fit into the intuition more accurately. At the same time, an improved contextual bisimulation is given by the means of Honda-Yoshida′s technique, which leads to a finer algebraic property. An example of firewall is provided to show the soundness of the improved calculus and its behavior equivalence.

关 键 词：移动计算 进程代数 安全环境演算 上下文互模拟 

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