中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 计算机科学国家重点实验室  > 学位论文
Subject: 计算机科学技术基础学科
Title:
基于带赋值符号迁移图的Monte Carlo模型检测
Author: 马明
Issued Date: 2012-05-31
Supervisor: 林惠民
Major: 计算机软件与理论
Degree Grantor: 中国科学院研究生院
Place of Degree Grantor: 北京
Degree Level: 硕士
Keyword: Monte Carlo 模型检测 ; 线性时序逻辑模型检测 ; 带赋值符号迁移图 ; 有导向的随机搜索 ; 启发式算法
Abstract: 随着计算机技术的快速发展,计算机软硬件系统的规模也急速增大,系统中会出现较多的错误和设计缺陷,这给系统的可靠性验证带来较大的难度。此外,一些安全攸关的系统(如电子商务系统、医疗仪器、以及汽车、飞机的控制系统等)在人们生活中也被广泛地应用,即使很小的设计缺陷或程序错误也会带来巨大的财力、物力损失甚至危及人们的生命安全。因此,如何保证系统的正确性和可靠性成为日益紧迫的问题。形式化验证技术凭借其数学和逻辑的严谨性,提供了一种验证系统正确性和可靠性的方法。作为其中的一种形式化验证技术,模型检测技术以其自动化程度高得到了人们的广泛关注和认可。然而,模型检测技术也面临“状态空间爆炸”问题的挑战。针对这一问题,一些研究人员提出了符号模型检测技术、偏序规约、对称规约以及限界模型检测技术等以缓解状态空间爆炸问题。  为了应对状态空间爆炸问题,研究人员也提出了一种基于假设检验和随机抽样的Monte Carlo模型检测技术。该技术是一种带单边误差的随机化算法,属于基于自动机理论的线性时序逻辑(LTL-Linear Temporal Logic)模型检测。算法运行速度快、节省内存,而且具有很好的可扩展性。然而,该算法采用均匀分布的随机搜索不一定非常高效地寻找到反例。因此,本文提出了一种新颖的结合带赋值符号迁移图和启发式搜索的模型检测算法,实现了基于该算法的验证工具,并使用几组程序实例进行了原Monte Carlo模型检测算法和本文提出的基于带赋值符号迁移图的启发式模型检测算法的对比实验。实验结果表明,将带赋值符号迁移图和表示性质公式否定式的自动机合成乘积Büchi自动机,并在其上执行有导向的随机搜索的启发式算法有效可行,提高了寻找反例的效率,显著地减少了在状态空间上搜索的状态数

量,从而缓解状态空间爆炸问题,提高模型检测的性能。

English Abstract: With the rapid development of computer technology, the hardware/software systems scale up fast. This results in the inevitable errors or defects in system design, thus rendering the verification of reliability of system difficult. Besides, due to the extensive applications of a range of safety-critical systems (such as electronic commerce systems, medical equipments as well as the control systems of automobiles and airplanes ) in daily life, some tiny program errors or design defects may engender enormous loss of financial and material resources, even the loss in people’s lives. Therefore, how to ensure the correctness and reliability of systems becomes increasingly urgent problems.Formal verification, depending on the rigorousness in mathematics and logics, provides one way to verify the correctness and reliability of systems. Among a variety of techniques of formal verification, model checking has been widely noticed and recognized because of its high level of automatization. However, model checking has been confronting the challenge of state space explosion. Aiming at this tough problem, researches proposed a number of techniques to curtail the state space explosion, such as symbolic model checking, partial order reduction, symmetry reduction and bounded model checking.In order to cope with the state space explosion problem, researchers proposed a method of Monte Carlo model checking based on hypothesis testing and random sampling, which is essentially a one-sided error randomized algorithm for automata-theoretic linear temporal logic model checking. Monte Carlo model checking runs fast, saves memory and scales extremely well. Despite this, random search with uniform distribution embedded in the Monte Carlo model checking algorithm cannot necessarily find the counterexample efficiently. Thus, a novel algorithm for model checking combining symbolic transition graph with assignment and heuristic search is proposed in this paper and a verification tool which the algorithm underlies is developed. Comparative verification experiments, between original Monte Carlo model checking and heuristic model checking based on symbolic transition graph with assignment, are conducted on a series of program examples. Results of verification experiments show this heuristic algorithm, implementing a guided random search in a product Büchi automaton constructed by a symbolic transition graph with assignment and an automaton representing the negation of the property, is feasible, valid and efficient to find counterexample and reduce significantly the number of states to be explored in the state space, thus curtailing state explosion and improving the performance of model checking.
 
Language: 中文
Content Type: 学位论文
URI: http://ir.iscas.ac.cn/handle/311060/14517
Appears in Collections:计算机科学国家重点实验室 _学位论文

Files in This Item:
File Name/ File Size Content Type Version Access License
12-5-31-最终答辩版论文.pdf(1771KB)----限制开放 联系获取全文

Recommended Citation:
马明. 基于带赋值符号迁移图的Monte Carlo模型检测[D]. 北京. 中国科学院研究生院. 2012-05-31.
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-2020  中国科学院软件研究所 - Feedback
Powered by CSpace