| π演算模型检测系统的设计与实现 |
| 方海
|
| 专业 | 计算机软件与理论
|
| 2000
|
| 学位授予单位 | 中国科学院软件研究所
|
| 学位 | 博士
|
| 学位授予地点 | 中国科学院软件研究所
|
| 关键词 | 形式化方法
自动验证
模型检测
Π演算
模态μ演算
|
| 摘要 | 模型检测技术是近十年来最成功的自动验证技术之一，目前已被广泛应用于有穷状态并发系统（包括电路设计和通讯协议等）的验证。π演算是一种表达能力很强的进程代数，能够用于刻划通信拓扑结构可动态变化的系统。模态μ演算是一种功能强大的时序逻辑，目前模型检测领域中使用的逻辑均可视为它的子逻辑。模型检测技术的最大障碍是状态爆炸问题－系统的状态数会随着系统的变元（包括相互作用的子系统以及值域复杂的数据结构）数呈指数增长。由于这一问题关系到模型检测技术在实际应用中能够处理的问题规模，因此寻找高效能行的算法已成为本领域的研究热点一。本文提出了一种基于一般传值系统的π演算局部模型检测算法，主要工作如下：●在模态μ演算的基础上给出了一种π演算的模态逻辑及其语义，和适用于π演算的模态逻辑图，并给出了基于符号迁移图和π演算模态逻辑图的模型检测算法●使用SML语言实现了该算法，构造了一个高效的模型检测工具。该系统能够根据π演算公式所描述的进程和嵌套等式系形式的模态μ演算公式描述的性质进行自动验证。 |
| 其他摘要 | Model-checking is one of the most successful automatic verfication techniques in the last decade. In has been used in verifying finite-state concurrent systems such as sequential circuit designs and communication protocols. The π-calculus is a very expressive process algebra, which can be used to describe systems with dynamically changing communication structures. The modal μ-calculus is a powerful temporal logic, almost every logic used in model-checking can be regarded as sub-logic of μ-calculus. The main challenge in model-checking is dealing with the state space explosion-the number of states would grow at an exponential rate as the number of variables, such as interacting subsystems or data structures that can assume many different states. As state explosion become the bottleneck and limited application of model-checking in practical-scale applications, this problem has been the hotspot in this area. This thesis presents a local model-checking algorithm for value-passing systems, including: ● A modal logic for π-calculus and its semantics are presented on the basis of modal μ-calculus, as well as the modal graph for π-calculus. And a model-checking algorithm is given which is based on symbolic transition graph and modal graph for π-calculus. ● An effective model checking system is constructed based on the implementation of the above algorithm in SML language. The system can automatically check whether given π-calculus agents have the properties described by recursive modal μ-calculus equations. |
| 页数 | 61
|
| 语种 | 中文
|
| 内容类型 | 学位论文
|
| URI标识 | http://ir.iscas.ac.cn/handle/311060/7494
|
| 专题 | 中科院软件所_中科院软件所
|
推荐引用方式
GB/T 7714 |
方海. π演算模型检测系统的设计与实现[D]. 中国科学院软件研究所. 中国科学院软件研究所,2000.
|
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论