近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进程的进程等式系作为该进程在模型检测器内部表示形式,从而将检测进程之间的结构同余关系转化为检查进程等式系之间的结构等价关系。本文实现了模型检测系统的原型系统,通过实验证明了实现框架和算法的有效性。总之,本文针对移动界程演算在移动计算系统形式化建模应用中的关键问题进行了探索,取得一定的成果。对于提高移动计算系统设计的可靠性,推动移动计算系统形式化建模应用具有重要的理论和应用价值。