中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
π演算模型检测系统的设计与实现
作者: 方海
答辩日期: 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.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7494
Appears in Collections:中科院软件所

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

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