| Title: | π-演算互模拟验证系统的设计与实现 |
| Author: | 许文
|
| Issued Date: | 2000
|
| Major: | 计算机软件与理论
|
| Degree Grantor: | 中国科学院软件研究所
|
| Place of Degree Grantor: | 中国科学院软件研究所
|
| Degree Level: | 博士
|
| Keyword: | 进程代数
; π-演算
; 互模拟
; 验证算法
|
| Abstract: | 进程代数是描述通讯并发系统的有效工具，π-演算中的通道通过传递通道名字可以改变系统的通信拓扑结构，因而非常适合描述通信拓扑结构可以动态改变的并发系统。互模拟关系是π-演算中研究的重要等价关系，研究自动验证互模拟关系的算法并建立相应的工具对π-演算应用于实际有着重要的意义。本文对π-演算中互模拟关系的自动验证算法和工具及相关应用进行了研究和探讨。本文中的主要工作有：1．互模拟验证算法的优化 在“模式互模拟”的基础上，提出了“紧模式互模拟”关系；并证明了模式互模拟和紧模式互模拟关系的等价性。根据紧模式互模拟得到了π-演算互模拟验证的优化算法，从而节省了验证所需的时间和空间。2．互模拟验证工具的实现 在传值CCS验证工具的基础上实现了π-演算的互模拟验证工具，对实现中的核心技术进行了一些探索。和国外同类工具相比，在许多实例上能达到更高的效率。3．对移动通信系统建模的尝试 对移动计算领域中的移动IP协议进行了建模并在系统中给予验证，建模中尝试了新的模型。 |
| English Abstract: | 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. |
| Language: | 中文
|
| Content Type: | 学位论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/6768
|
| Appears in Collections: | 中科院软件所
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| LW002149.pdf（1542KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
许文. π-演算互模拟验证系统的设计与实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000-01-01.
|
|
|
