π-演算互模拟验证系统的设计与实现
文献类型:学位论文
作者 | 许文 |
学位类别 | 博士 |
答辩日期 | 2000 |
授予单位 | 中国科学院软件研究所 |
授予地点 | 中国科学院软件研究所 |
关键词 | 进程代数 π-演算 互模拟 验证算法 |
学位专业 | 计算机软件与理论 |
中文摘要 | 进程代数是描述通讯并发系统的有效工具,π-演算中的通道通过传递通道名字可以改变系统的通信拓扑结构,因而非常适合描述通信拓扑结构可以动态改变的并发系统。互模拟关系是π-演算中研究的重要等价关系,研究自动验证互模拟关系的算法并建立相应的工具对π-演算应用于实际有着重要的意义。本文对π-演算中互模拟关系的自动验证算法和工具及相关应用进行了研究和探讨。本文中的主要工作有:1.互模拟验证算法的优化 在“模式互模拟”的基础上,提出了“紧模式互模拟”关系;并证明了模式互模拟和紧模式互模拟关系的等价性。根据紧模式互模拟得到了π-演算互模拟验证的优化算法,从而节省了验证所需的时间和空间。2.互模拟验证工具的实现 在传值CCS验证工具的基础上实现了π-演算的互模拟验证工具,对实现中的核心技术进行了一些探索。和国外同类工具相比,在许多实例上能达到更高的效率。3.对移动通信系统建模的尝试 对移动计算领域中的移动IP协议进行了建模并在系统中给予验证,建模中尝试了新的模型。 |
语种 | 中文 |
公开日期 | 2011-03-17 |
页码 | 55 |
源URL | [http://ir.iscas.ac.cn/handle/311060/6768] ![]() |
专题 | 软件研究所_中科院软件所_中科院软件所 |
推荐引用方式 GB/T 7714 | 许文. π-演算互模拟验证系统的设计与实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000. |
入库方式: OAI收割
来源:软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。