基于带赋值符号迁移图的Monte Carlo模型检测

CORC > 软件研究所 > 计算机科学国家重点实验室 > 学位论文

题名

基于带赋值符号迁移图的Monte Carlo模型检测

作者

马明

学位类别

硕士

答辩日期

2012-05-31

授予单位

中国科学院研究生院

授予地点

北京

导师

林惠民

关键词

Monte Carlo 模型检测线性时序逻辑模型检测带赋值符号迁移图有导向的随机搜索启发式算法

学位专业

计算机软件与理论

中文摘要

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

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

英文摘要

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.

语种

中文

学科主题

计算机科学技术基础学科

公开日期

2012-06-13

内容类型

学位论文

源URL

[http://ir.iscas.ac.cn/handle/311060/14517]