界程演算模型检测

摘要

本文的研究工作主要有以下几个方面； 1. 在界程演算方面。由于在移动界程(Mobile Ambients，MA)中，in、out、open操作可以不受限进行，环境对自身边界没有任何管理权限，并且由于MA中open操作的存在，两个原本不在一块的进程能通过open操作后处在同一环境中，这样可导致两个进程间意想不到的交互(干扰)的产生。为了克服这些不足，安全环境演算(Safe Ambients，SA)中增加了in、out、open协操作，分别是对in、out、open操作的许可；带口令的安全界程演算(Safe Ambients with Password，SAP)SAP在in、out，open、in、out、open操作中增加口令(或通道>，只有掌握口令(或通道)的进程才能进行in、out、open操作；盒子界程演算(Boxed Ambients，BA)中取消了open操作，同时增加了父子界程间能够跨界程通信的操作原语。SA、SAP和BA都是对MA演算的改进，但都只是局部的改进，最终SA、SAP不能避免由于open操作带来的干扰，BA也控制不了in和out操作对界程边界的随意穿越。同时由于BA中无open操作，界程一旦建立，将永远停留在系统中，这样将占用大量的系统资源，也不符合进程的实际情况。为了克服MA、SA、SAP和BA的不足，本文提出了一个带口令的安全盒子界程演算(Safe Boxed Ambients with Password，SBAP)。相对于MA，BSAP做了如下几点改进；(1)取消了MA中的open操作，增加了父子界程间的通信操作原语；(2)增加了in、out操作，并在in、out、in、out操作中加入了密码；(3)增加了界程回收操作原语del。通过用SBAP对Internet上的电子邮件系统进行描述和仿真以及对进程死锁的实时处理，说明SBAP在网络计算方面有一定的表现能力。 2.在mu-演算模型检测方面。针对完全μ-演算的全局模型检测算法的设计，根据Tarski's不动点定理，公式中的不动点算子直接用逐次迭代来计算，则对有不动点算子嵌套的逻辑表达式进行计算的全局算法的时间复杂性为O(nk+1)，其中n为变迁系统的状态总数，k为不动点算子嵌套深度。Long等人在分析了计算嵌套不动点表达式的中间结果间的偏序关系找到了一个时间复杂性为O(n[d/2]+1)，空间复杂性为指数的全局计算算法。本文在Long等人工作的基础上，根据μ-演算公式中函数的单调特性，提出了一个时间复杂性为O((2n+1)[(d+3)/4]+[(d+2)/4])，空间复杂性为O(dn)的计算交替嵌套μ-演算公式的全局模型检测算法，在目前已知的针对完全μ-演算的全局模型检测算法中是首个空间复杂性为O(dn)且时间复杂性指数部分只有d／2的算法。算法性能的改善，使得不动点算子交替嵌套深度很大的μ-演算公式的求解成为可能，这在模型检测方面有着非常重要的意义。 3.在界程逻辑模型检测方面。本文在林惠民院士的工作基础上，讨论了带递归的谓词界程逻辑在有限控制移动界程上的模型检测问题，首次将嵌套谓词等式系应用到带递归的谓词界程逻辑模型检测中，提出了一个时间复杂性与逻辑公式的交错嵌套深度呈指数关系的局部模型检测算法，这是目前首个有明确时间复杂性的谓词界程逻辑模型检测算法，也是目前已知的第二个带递归的谓词界程逻辑模型检测算法。所做的工作主要有：(1)讨论了谓词界程逻辑公式与嵌套谓词等式系间语义的等价性，给出了谓诃界程逻辑公式转换成嵌套谓词等式系的方法；(2)讨论了不动点算子无交错的谓词界程逻辑模型检测问题，给出了具体算法；(3)讨论了不动点算子交错嵌套情况下的谓词界程逻辑模型检测问题，给出了一个通用的局部算法。

目录

文摘

英文文摘

声明

第一章引言

1.1并发系统

1.2形式化验证方法

1.3 Kripke结构和标号迁移系统

1.4模型检测

1.5模型检测举例——基于PI演算的安全协议分析[江华08b]

1.5.1 Station-to-station协议

1.5.2 安全协议的π-演算描述

1.5.3 Station-To-Station协议验证

1.6本文工作和论文结构

第二章进程演算

2.1 CCS和π-演算

2.1.1 CCS

2.1.2 π-演算

2.2界程演算

2.3安全界程演算[Lev00,Lev03]

2.4带口令的安全界程演算[Mer02]

2.5盒子界程演算[Bug01]

2.6带口令的安全盒子界程演算[江华07,Jia07,Jia08b]

2.6.1带口令的安全盒子界程演算的定义

2.6.2带口令的安全盒子界程演算的应用

2.7本章小结

第三章逻辑

3.1 Hennessy-Hilner逻辑[Hen00]

3.2命题模态μ-演算[Sti96,Sti01]

3.3界程逻辑

3.4嵌套谓词等式系

3.4.1嵌套谓词等式系语法

3.4.2嵌套谓词等式系语义

5本章小结

第四章命题mu演算模型检测

4.1概述

4.2模型检测算法基本思想

4.3模型检测算法正确性分析

4.4算法扩展

4.4.1通用模型检测算法

4.4.2最外层不动点是ν的算法扩展

4.5模型检测算法复杂性分析

4.6举例

4.7本章小结

第五章界程逻辑模型检测

5.1背景

5.2不动点算子无交错嵌套的界程逻辑模型检测

5.2.1不动点算子无交错嵌套的界程逻辑公式转换为嵌套谓词等式系

5.2.2不动点算子无交错的嵌套谓词等式系的求解

5.2.3不动点算子无交错嵌套的界程逻辑模型检测算法复杂性分析

5.2.4举例

5.3不动点算子交错嵌套的界程逻辑模型检测

5.3.1不动点算子交错嵌套的界程逻辑模型检测算法设计

5.3.2不动点算子交错嵌套的界程逻辑模型检测算法复杂性分析

5.4算法改进

5.4.1界程逻辑公式直接转换为嵌套谓词等式系

5.4.2界程逻辑模型检测算法改进

5.4.3改进算法复杂性分析

5.5本章小结

第六章工作总结与展望

6.1相关工作总结

6.1.1在界程演算方面的工作

6.1.2在mu-演算模型检测方面的工作

6.1.3在界程逻辑模型检测方面的工作

6.2进一步的工作展望

致谢

参考文献

附录A：作者在学习期间完成的论文