移动界程演算及模型检测应用的关键问题研究

发布时间：2020-07-24 05:49

【摘要】： 近10年来,以界程演算(Mobile Ambients)为代表移动进程演算模型已成为移动计算形式化理论的研究热点,但相对于理论研究方面的丰富成果,模型实用化方面研究相对较少,特别是将界程演算实际应用于移动计算系统的核心程序语言,或系统建模语言的应用界程演算模型,以及相关模型检测系统的实现等方面还有待进一步研究。本文针对上述问题,在面向移动计算系统建模应用的扩展界程演算、界程演算的空间逻辑、偏序模型检测方法以及模型检测系统实现框架等方面进行了研究。主要工作包括: 1、提出了以“界程”为核心概念的、面向移动计算系统建模应用的扩展演算模型。本文针对移动计算系统的建模语言需要表达IF-THEN-ELSE语义以及模型性质的自动验证需要系统模型保持有限状态性质这一命题进行了研究,提出了一种扩展界程演算模型--应用界程演算(简称Applied-AC演算)。该演算首先在现有界程扩展演算中引入IF-THEN-ELSE结构的进程,并采用带参数的递归进程结构来表示进程的重复执行。该演算引入一种标准化操作来处理IF-THEN-ELSE结构进程的语义,简化了模型检测时空间逻辑语义的复杂性。该演算还研究了Applied-AC演算的有限控制进程的问题,采用类型系统来保证Applied-AC进程在基于结构同余所确立的等价关系下的有限控制性,并研究了有限控制的Applied-AC演算对有限PI演算进程的翻译方法。本文采用的类型系统和有限控制界程演算对有限PI演算的翻译方法可推广应到到其它所有含有协动作原语的界程演算扩展模型。 2、提出了一种可判定的、融合了空间模态和行为模态的空间逻辑。针对空间逻辑中的并发模态副词是观察进程交互行为的关键因素,但引入并发模态副词又导致模型检测的不可判定性这一问题。提出了一种可判定的、融合了空间模态和行为模态思想的应用界程逻辑,并给出该逻辑在Applied-AC演算下的逻辑语义及模型检测算法。本文还分析了Applied-AC演算进程在应用界程逻辑下的逻辑等价与结构同余之间的包含关系,表明了运用逻辑等价方式能够以更抽象的层次来观察进程行为等价性质。 3、提出了Applied-AC演算进程在应用界程逻辑下采用偏序方法进行模型检测的算法。本文分析了在应用界程演算和应用界程逻辑下采用偏序方法进行模型检测所面临的问题;研究了Applied-AC进程偏序合流归约应具有的性质以及影响进程满足偏序合流归约的各种因素,从而给出了判别进程偏序合流归约的充分性条件。研究了应用界程逻辑公式与进程偏序合流归约造成的进程空间性质变化之间的关系,得到空间逻辑公式对进程偏序合流归约行为不可观察的充分性条件。给出判别在Applied-AC演算下进行模型检测中是否能够运用偏序方法来验证逻辑性质的方法,及其实现算法。实验结果表明本文给出的算法在验证模型的死锁性和安全性方面能够较大程度上减轻状态爆炸的现象。 4、给出了实现模型检测系统的关键数据结构和算法并实现了原型系统。进程之间结构同余关系的判定算法和数据结构是实现空间模型检测系统所面临的主要问题。Applied-AC演算引入带参数的递归进程和条件选择进程后,递归进程的执行将不再仅仅是单一进程实例的简单重复,在模型检测器内部进程不能直接采用单一的树型结构来表示。针对这个问题,本文设计了Applied-AC进程的进程等式系作为该进程在模型检测器内部表示形式,从而将检测进程之间的结构同余关系转化为检查进程等式系之间的结构等价关系。本文实现了模型检测系统的原型系统,通过实验证明了实现框架和算法的有效性。总之,本文针对移动界程演算在移动计算系统形式化建模应用中的关键问题进行了探索,取得一定的成果。对于提高移动计算系统设计的可靠性,推动移动计算系统形式化建模应用具有重要的理论和应用价值。
【学位授予单位】：华南理工大学
【学位级别】：博士
【学位授予年份】：2010
【分类号】：TP338
【图文】：

主机,通道,运行时,移动代理

图 2-1在通道界程系统中，每个主机都安装有运行时系统（RunningtimeSystem）来解移动代理的通讯、移动动作等。计算实体之间的通讯、移动交互原则：只有邻近的计算实体之间才可以直接交是说，LAN 内主机不能直接与另一 LAN 中的主机交互，而必须借助于承担网主机。类似地，移动代理也不能直接与另一代理内部的模块直接交互，而需要理责任的代理；一个模块也不能直接存取另一个模块的内部私有数据，而需要块的接口。计算实体进程的通讯、移动交互都由命名的通道上完成。即主机之间由 TCP议提供的网络信道来完成，移动代理之间、或模块之间由主机内部网络端口来2、通道界程演算通道界程演算（CA演算）是根据通道界程系统的通讯、交互方式，并在BoxedAm基础上扩展得到的演算模型。主要的语法和语义如下：

【参考文献】