π演算模型检测系统的设计与实现
文献类型：学位论文
| 作者 | 方海 |
| 学位类别 | 博士 |
| 答辩日期 | 2000 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 形式化方法 自动验证 模型检测 π演算 模态μ演算 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 模型检测技术是近十年来最成功的自动验证技术之一，目前已被广泛应用于有穷状态并发系统（包括电路设计和通讯协议等）的验证。π演算是一种表达能力很强的进程代数，能够用于刻划通信拓扑结构可动态变化的系统。模态μ演算是一种功能强大的时序逻辑，目前模型检测领域中使用的逻辑均可视为它的子逻辑。模型检测技术的最大障碍是状态爆炸问题－系统的状态数会随着系统的变元（包括相互作用的子系统以及值域复杂的数据结构）数呈指数增长。由于这一问题关系到模型检测技术在实际应用中能够处理的问题规模，因此寻找高效能行的算法已成为本领域的研究热点一。本文提出了一种基于一般传值系统的π演算局部模型检测算法，主要工作如下：●在模态μ演算的基础上给出了一种π演算的模态逻辑及其语义，和适用于π演算的模态逻辑图，并给出了基于符号迁移图和π演算模态逻辑图的模型检测算法●使用SML语言实现了该算法，构造了一个高效的模型检测工具。该系统能够根据π演算公式所描述的进程和嵌套等式系形式的模态μ演算公式描述的性质进行自动验证。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 61 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/7494]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 方海. π演算模型检测系统的设计与实现[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2000. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。