中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
π-演算互模拟验证系统的设计与实现
作者: 许文
答辩日期: 2000
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 进程代数 ; π-演算 ; 互模拟 ; 验证算法
摘要: 进程代数是描述通讯并发系统的有效工具,π-演算中的通道通过传递通道名字可以改变系统的通信拓扑结构,因而非常适合描述通信拓扑结构可以动态改变的并发系统。互模拟关系是π-演算中研究的重要等价关系,研究自动验证互模拟关系的算法并建立相应的工具对π-演算应用于实际有着重要的意义。本文对π-演算中互模拟关系的自动验证算法和工具及相关应用进行了研究和探讨。本文中的主要工作有:1.互模拟验证算法的优化 在“模式互模拟”的基础上,提出了“紧模式互模拟”关系;并证明了模式互模拟和紧模式互模拟关系的等价性。根据紧模式互模拟得到了π-演算互模拟验证的优化算法,从而节省了验证所需的时间和空间。2.互模拟验证工具的实现 在传值CCS验证工具的基础上实现了π-演算的互模拟验证工具,对实现中的核心技术进行了一些探索。和国外同类工具相比,在许多实例上能达到更高的效率。3.对移动通信系统建模的尝试 对移动计算领域中的移动IP协议进行了建模并在系统中给予验证,建模中尝试了新的模型。
英文摘要: Process algebras are mathematical theories for communicating concurrent systems. In π-calculus, channels can send channel names, which can change the communication structure of the system, therefore π-calculus is very useful in describing systems with dynamically changing communication structures. Bisimulation is one of the important equivalent relations studied in π-calculus. Considering the complexity of the systems to be modeled, the research on automatic verification algorithms and tools plays an important role in the application of π-calculus. Bisimulation checking algorithms and system implementations are studied in this thesis. The main work in this thesis include: 1. Optimization of bisimulation checking algorithm Tight Schematic Bisimulation is presented which is based on the original definition of Schematic Bisimulation, and equality between the two relations proved. Based on the definition of the new relation, an optimized bisimulation checking algorithm is obtained; it can reduce the time and space needed in verification. 2. Implementation of bisimulation checking system We implemented a bisimulation checking system for the π-calculus is implemented on the basis of the original CCS version. Its main functionality is to check late and early bisimulation (strong and weak) using the algorithms presented. 3. The attempt in modeling mobile communicating systems In the modeling of Mobile IP protocol, we tried to give a different model to describe the "mobility" of the system. As an example, Mobile IP protocol is modeled and verified.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6768
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW002149.pdf(1542KB)----限制开放-- 联系获取全文

Recommended Citation:
许文. π-演算互模拟验证系统的设计与实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[许文]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[许文]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace