基于反例搜索的启发式模型检测算法的研究
文献类型：学位论文
| 作者 | 施小纯 |
| 学位类别 | 博士 |
| 答辩日期 | 2004 |
| 授予单位 | 中国科学院软件研究所 |
| 授予地点 | 中国科学院软件研究所 |
| 关键词 | 形式化方法 模型检测 线性时序逻辑 遗传算法 启发式信息 |
| 其他题名 | A Heuristic Algorithm for Model-Checking Based on Counter Example Finding |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 模型检测技术是最近二十年来最成功的自动验证技术之一，目前已经被广泛地应用于有穷状态系统（包括电路设计和通信协议）的分析与验证。由于这一技术是基于对状态空间的穷尽搜索，“状态爆炸”问题一直是制约其在实际系统中应用的主要技术瓶颈。对于大规模系统，由于受到内存空间的l浪制，模型检测技术往往难以完成对系统状态空间的穷尽搜索，而一般的随机搜索算法对于寻找系统中可能存在的错误的搜索效率极低。为了在时空效率方面取得一个较好的平衡点，本文提出了一种基于启发式信，豁狗解决方案，其要点为：以Krinke结构为并发系统的模型，使用线性时序逻辑LTL来描述系统所期望的性质，将该公式取反后得到反例路径的LTL公式；通过计算一条路径满足的该公式的最大结构复杂度，我们判定所采集的路径在多大程度上“符合”所描述的反例特征，由此实现对搜索方向的引导。通过类似遗传算法的搜索流程，我们期望能够尽快的找到可能存在的错误。实例研究表明，对标准的模型检测工具无法处理的大型系统，本文所提出的方法能以较好的概率发现隐藏的错误，并给出相应的诊断信息。论文的主要工作如下：·设计了基于LTL路径公式的启发式信息，以及选择，交叉，变异等进化操作。·根据所设计的启发式搜索算法，实现了相应的原型工具。·通过实例研究证明了算法的有效性。 |
| 语种 | 中文 |
| 公开日期 | 2011-03-17 |
| 页码 | 43 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/5624]  |
| 专题 | 软件研究所_中科院软件所_中科院软件所 |
| 推荐引用方式 GB/T 7714 | 施小纯. 基于反例搜索的启发式模型检测算法的研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 2004. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。