中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
井发传值进程模型检测工具的数据类型扩展
作者: 张轶
答辩日期: 2003
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 形式化方法 ; 模型检侧 ; 并发传值进程 ; 复杂数据类型 ; 传值CCS ; 带赋值符号迁移图
其他题名: Extending a Model-Checking Tool with Non-trivial Data Structures
摘要: 模型检测技术是近二十年来最成功的自动验证技术之一,目前被广泛的应用于有穷状态系统(包括电路设计和通讯协议等)的分析与验证。对于并发传值系统的自动分析与验证是模型检测研究的一个新的方向。随着并发系统规模的日益增大,对这类系统的模型检测面临着如何处理大规模状态空间问题的挑战,因此需要为实际的大规模并发系统精心选择计算模型,同时设计时空效率较高的算法。但是我们注意到并发传值系统的一个特点是其子系统间的通讯经常涉及复杂数据结构,包括数组、列表和记录等。以往处理复杂数据结构的做法是抽象掉数据信息或者将复杂数据结构打散,因而较大的影响了检测效率。解决这个问题的一个方案是:使用带赋值符号迁移图(STGA)作为并发传值进程的模型,使用谓词p演算作为刻画性质的逻辑,并采用动态实例化的算法对传值并发进程直接进行模型检测。本文提出了将复杂数据结构引入上述模型检测方案的办法,扩大了该解决方案可以应用的问题领域。主要工作如下:扩展传值CCS使其成为有严格类型规则的易于使用的系统描述语言、扩充了STGA的定义和生成规则使其适于作为实际系统的计算模型。提出了扩展STGA图的优化算法。扩充检测问题的定义语言一脚本语言的格式,使用SML语言实现了脚本语言的编译和扩展STGA图生成模块,并将该模块和检测算法核心连接,实现了整个工具。论文还结合应用实例证明了扩展工作的有效性并分析了工具的性能。
英文摘要: Model-checking is one of the most successful automatic verification techniques in the past two decades. It has been used in the analysis and verification of finite-state systems such as sequential circuit designs and communication protocols. Analyzing and verifying value-passing concurrent systems is a new research area in model-checking. With the rapid increase in the concurrent systems' scales, a challenging issue facing model-checking researchers is how to handle the huge state spaces. Thus it becomes increasingly important to develop suitable computation models and to design efficient verification algorithms. An important feature of value-passing systems concurrent is that it is always involving non-trivial data structures when several subsystems communicate with each other. Here, non-trivial data structures may include arrays, lists and records. The traditional approaches to handle non-trivial data structures are either abstracting them from system models or expanding them into non-structural data, which often reduces the efficiency of verification substantively. A possible solution to this problem is: adopting Symbolic Transition Graph with Assignment (STGA for short) to model value-passing systems, introducing a predicate mu-calculus to characterize desired properties, and verifying value-passing concurrent processes using an "on-the-fly" algorithm. This thesis presents a way to introduce non-trivial data structures into the solution mentioned above, which helps to extend its application domain. The work includes: Extending value-passing CCS to a system description language with strict typing rules; Extending accordingly the definition and generation rules of the basic STGA, which makes it suitable for modeling real systems. Presenting optimization algorithms for extended STGA Extending the syntax of the script language to definite the verification problem, and imple menting the compilation and STGA generation module for this language; Incorporating the module with the core verification algorithm; demonstrating the validation and analyzing the performance of the tool with some real-world examples.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/7390
Appears in Collections:中科院软件所

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

Recommended Citation:
张轶. 井发传值进程模型检测工具的数据类型扩展[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2003-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