中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于反例搜索的启发式模型检测算法的研究
作者: 施小纯
答辩日期: 2004
专业: 计算机软件与理论
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 形式化方法 ; 模型检测 ; 线性时序逻辑 ; 遗传算法 ; 启发式信息
其他题名: A Heuristic Algorithm for Model-Checking Based on Counter Example Finding
摘要: 模型检测技术是最近二十年来最成功的自动验证技术之一,目前已经被广泛地应用于有穷状态系统(包括电路设计和通信协议)的分析与验证。由于这一技术是基于对状态空间的穷尽搜索,“状态爆炸”问题一直是制约其在实际系统中应用的主要技术瓶颈。对于大规模系统,由于受到内存空间的l浪制,模型检测技术往往难以完成对系统状态空间的穷尽搜索,而一般的随机搜索算法对于寻找系统中可能存在的错误的搜索效率极低。为了在时空效率方面取得一个较好的平衡点,本文提出了一种基于启发式信,豁狗解决方案,其要点为:以Krinke结构为并发系统的模型,使用线性时序逻辑LTL来描述系统所期望的性质,将该公式取反后得到反例路径的LTL公式;通过计算一条路径满足的该公式的最大结构复杂度,我们判定所采集的路径在多大程度上“符合”所描述的反例特征,由此实现对搜索方向的引导。通过类似遗传算法的搜索流程,我们期望能够尽快的找到可能存在的错误。实例研究表明,对标准的模型检测工具无法处理的大型系统,本文所提出的方法能以较好的概率发现隐藏的错误,并给出相应的诊断信息。论文的主要工作如下:·设计了基于LTL路径公式的启发式信息,以及选择,交叉,变异等进化操作。·根据所设计的启发式搜索算法,实现了相应的原型工具。·通过实例研究证明了算法的有效性。
英文摘要: Model-checking is one of the most successful automatic verification tecliniques 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. Because it is based on the exhaustive state space search, the state space explosion problem becomes the primary bottleneck when we apply model-checking to real systems. For systems with large state spaces, model checking technique may fail to finish the systems' verification due to the limitation of memory. On the other hand, random search algorithm could not find the potential errors effectively. In order to obtain a reasonable balance between memory usage and time expense, we present a possible solution based on heuristic information: we model the system as a Kripke structure and desired properties are expressed by LTL formulas. The LTL path formula in the negation of the original LTL formula describes the character of counter examples. Inspired by the idea of genetic algorithms, we proposed to use the "maximal structural complexity " of the subformulas satisfied in a path as heuristic information to guide the search direction. By case study, we demonstrate the heuristic algorithm can find the potential errors effectively and return responding diagnostic information, especially for large systems that are difficult to be verified by normal model-checking tool. The work includes: Designing the heuristic information based on Linear Temporal Logic, and some genetic operators, for example, select, across and mutate. Implementing prototypal tool based on the heuristic algorithm. Demonstrating the validation of the algorithm with a example.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/5624
Appears in Collections:中科院软件所

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

Recommended Citation:
施小纯. 基于反例搜索的启发式模型检测算法的研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004-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