| Title: | 基于反例搜索的启发式模型检测算法的研究 |
| Author: | 施小纯
|
| Issued Date: | 2004
|
| Major: | 计算机软件与理论
|
| Degree Grantor: | 中国科学院软件研究所
|
| Place of Degree Grantor: | 中国科学院软件研究所
|
| Degree Level: | 博士
|
| Keyword: | 形式化方法
; 模型检测
; 线性时序逻辑
; 遗传算法
; 启发式信息
|
| Alternative Title: | A Heuristic Algorithm for Model-Checking Based on Counter Example Finding
|
| Abstract: | 模型检测技术是最近二十年来最成功的自动验证技术之一，目前已经被广泛地应用于有穷状态系统（包括电路设计和通信协议）的分析与验证。由于这一技术是基于对状态空间的穷尽搜索，“状态爆炸”问题一直是制约其在实际系统中应用的主要技术瓶颈。对于大规模系统，由于受到内存空间的l浪制，模型检测技术往往难以完成对系统状态空间的穷尽搜索，而一般的随机搜索算法对于寻找系统中可能存在的错误的搜索效率极低。为了在时空效率方面取得一个较好的平衡点，本文提出了一种基于启发式信，豁狗解决方案，其要点为：以Krinke结构为并发系统的模型，使用线性时序逻辑LTL来描述系统所期望的性质，将该公式取反后得到反例路径的LTL公式；通过计算一条路径满足的该公式的最大结构复杂度，我们判定所采集的路径在多大程度上“符合”所描述的反例特征，由此实现对搜索方向的引导。通过类似遗传算法的搜索流程，我们期望能够尽快的找到可能存在的错误。实例研究表明，对标准的模型检测工具无法处理的大型系统，本文所提出的方法能以较好的概率发现隐藏的错误，并给出相应的诊断信息。论文的主要工作如下：·设计了基于LTL路径公式的启发式信息，以及选择，交叉，变异等进化操作。·根据所设计的启发式搜索算法，实现了相应的原型工具。·通过实例研究证明了算法的有效性。 |
| English Abstract: | 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. |
| Language: | 中文
|
| Content Type: | 学位论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/5624
|
| Appears in Collections: | 中科院软件所
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| LW014041.pdf（2464KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
施小纯. 基于反例搜索的启发式模型检测算法的研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004-01-01.
|
|
|
