高级检索

    Ambient演算的一种分层语义

    A Denotational Semantic Description for Safe Ambient Calculus

    • 摘要: 网络计算系统中涉及的操作复杂,很难直接给出一种的语义描述框架.作为一种网络计算模型,Ambient演算主要刻画了计算的分布性和移动性.目前关于Ambient的语义研究很多,但均是基于规约规则的语义形式.这种描述方式尽管简洁,一方面却具有不确定性,不利于实际的网络计算系统的设计和直接实现;另一方面,这种语义描述方式均在一个层次上描述Ambient演算系统中的各种行为语义,使得Ambient演算中各种计算行为纠缠在一起,复杂而难以理解.根据Ambient演算的结构特点,给出了Ambient演算的一种分层语义描述形式,系统以ambient为单元,分成3层进行描述,分别给出不同层上行为的语法定义、语义定义、语义方程以及不同层间的转换函数的定义,从而给出Ambient演算系统的指称语义描述形式.这种描述方式从层次化的角度分析了Ambient演算的计算行为,有助于对Ambient演算中行为的理解和实际应用系统的实现.

       

      Abstract: Since computation under network involves variants, complicated information and behaviors, it is difficult to give denotational semantic description for computing under network. As a kind of network computing model, Ambient calculus contributes to modeling mobility and distributed features of network computing. Researches on its semantics description are mostly based on reduction rules. These descriptions are brief, but based on them it is indeterminable and has disadvantage in system design and direct implementation. On the other hand, these works mostly focus on describing variants behaviors of Ambient calculus in one level, which makes it complicated to understand clearly how these variants behaviors work and how they work together. As a result, based on the unit ambient of Ambient calculus, a three-level semantics description framework is given for Ambient calculus. The three levels are: internal level of ambient, ambient level, and system level. For each of these three levels, the syntax and semantics of its behaviors is defined in detail, and the transformation relation functions between each two levels are given. In order to specify how the framework works, a practical example is given based on this framework in three levels. Finally, proof is shown to prove the correctness of this semantic framework. This layered semantics description may help users analyze behaviors of computing in Ambient calculus and understand the implementation of ambient practical systems.

       

    /

    返回文章
    返回