一种基于Büchi自动机的LTL程序模型检测方法

时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。基于自动机的理论,用标签转移系统（S）表示程序的行为,用时序逻辑公式（F）描述程序的性质,构建相应的Büchi自动机,从而证明形式化公式SF是否可满足。     

基于线性时态逻辑的Petri网模型检测研究

线性时态逻辑Petri网结合了Petri网和时序逻辑的优点,清晰简洁的描述并发系统事件间的时序和因果关系,包括系统的活性和安全性.其中自动机的体积是模型检验的一个关键性问题,为了得到尽可能小体积的自动机,在LTL公式转换为Büchi自动机之前,对LTL公式进行预处理来减少冗余,然后通过布尔技术优化自动机.     

基于SCC空性检测中状态空间的缩减方法

对Couvreur提出的基于强连通图的空性检测算法进行改进,使基于嵌套的深度优先搜索与基于强连通图搜索算法的优势结合起来,在对基于迁移的扩展(具有多个可接受条件)Büchi自动机进行空性检测过程中,使用一个布尔变量标识一个状态,不仅节省了内存消耗,而且一般情况下的性能明显优于已有的算法,最坏情况等同于Couvreur的算法.同时反例寻找过程等同于基于强连通图的检测算法.     

从基于迁移的扩展Büchi自动机到Büchi自动机

目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(linear temporal logic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-based generalized Büchi automaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.     

基于模型的机组组合两阶段启发式算法

针对同时考虑机组爬坡速率约束和系统安全约束的机组组合问题,提出一个基于模型的两阶段启发式算法.第1阶段确定可行的机组启停状态,首先构造初始启停状态,并根据模型检验初始启停状态是否可行,如果不可行,则通过目标函数的线性近似和约束松弛构造问题的松弛模型,并将其用于可行化机组的启停状态;第2阶段利用经济分配模型确定机组的输出功率.基于118-母线电力系统的测试验证了所提出算法的有效性和鲁棒性.     

Büchi自动机的优化综述

对Büchi自动机进行优化是提高基于自动机的模型检测效率的重要手段.对直接模拟关系、延迟模拟关系和公平模拟关系的概念,进行了比较,并探讨了基于这些模拟关系的自动机优化方法.基于左右语言的优化是完全基于自动机理论的优化方法,于是深入探讨了利用左右语言对Büchi自动机的优化绍方法.最后对未来的研究方向作了简要的介绍.     

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画.为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题.一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范;另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画.针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法.模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机;接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中;最后对该乘积自动机进行判空检测.与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证.     

分布式数据库数据分布模型的启发式算法

本文提出了以最小代价为目标的分布式数据库数据分布模型求解的启发式算法，利用数据分布的启发信息，将互相有紧密联系的ｎ个关系的数据分布问题分解为具有较松散联系的ｎ个关系的分布问题，并进行迭代调整，使算法的时间复杂度大为降低，算法精度也接近优化程度。     

求解HP模型蛋白质折叠问题的启发式算法

构造了一个新的数学模型,把三维HP模型的蛋白质折叠问题由一个有约束的优化问题转化为无约束的优化问题,通过建立相对坐标和邻域结构,提出了一个局部搜索算法,并对文献中的链长不同的7个算例进行了测试。结果表明,该算法能在较短时间内找到其中5个算例的最优能量枸形,对另外2个难例,则可以找到能量仅比最优构形高一个单位的次优构形。     

一种基于LIP模型的边缘检测新算法

提出了一种基于人眼视觉的图像边缘检测的新算法。该方法基于LIP模型首先推导出新的梯度公式,然后进行图像灰度处理和叠加操作,最终形成了一种新的边缘检测算法。该方法大大减少了非边缘噪声的产生,能将图像的边缘较好地检测出来。实验表明,该方法具有边缘检测准确性高,引入的非边缘噪声少的特点。     

Model Checking of Safety Properties

Of special interest in formal verification are safety properties, which assert that the system always stays within some allowed region. Proof rules for the verification of safety properties have been developed in the proof-based approach to verification, making verification of safety properties simpler than verification of general properties. In this paper we consider model checking of safety properties. A computation that violates a general linear property reaches a bad cycle, which witnesses the violation of the property. Accordingly, current methods and tools for model checking of linear properties are based on a search for bad cycles. A symbolic implementation of such a search involves the calculation of a nested fixed-point expression over the system's state space, and is often infeasible. Every computation that violates a safety property has a finite prefix along which the property is violated. We use this fact in order to base model checking of safety properties on a search for finite bad prefixes. Such a search can be performed using a simple forward or backward symbolic reachability check. A naive methodology that is based on such a search involves a construction of an automaton (or a tableau) that is doubly exponential in the property. We present an analysis of safety properties that enables us to prevent the doubly-exponential blow up and to use the same automaton used for model checking of general properties, replacing the search for bad cycles by a search for bad prefixes.     

Bisimulation Minimization and Symbolic Model Checking

State space minimization techniques are crucial for combating state explosion. A variety of explicit-state verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. Experimental results on bisimulation minimization in symbolic model checking contexts, however, are mixed. This paper explores bisimulation minimization as an optimization in symbolic model checking of invariance properties. We consider three bisimulation minimization algorithms. From each, we produce a BDD-based model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, suggest that bisimulation minimization is not viable in the context of invariance verification, because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability.     

Termination Criteria for Bounded Model Checking: Extensions and Comparison

Increasing attention has been paid recently to criteria that allow one to conclude that a structure models a linear-time property from the knowledge that no counterexamples exist up to a certain length. These termination criteria effectively turn Bounded Model Checking into a full-fledged verification technique and sometimes result in considerable time savings. In [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] we presented a criterion based on the translation of the linear-time specification into a Büchi automaton. BMC can be terminated if no fair cycle is found up to a given length, and one can prove that no fair cycle exists beyond that length. The maximum length for which counterexamples are explicitly checked is called the termination length; it obviously depends on the model, the property, and the termination criterion. In this paper we improve the criterion of [M. Awedh and F. Somenzi. Proving more properties with bounded model checking. In R. Alur and D. Peled, editors, Sixteenth Conference on Computer Aided Verification (CAV'04), pages 96–108. Springer-Verlag, Berlin, July 2004. LNCS 3114] by adding a check that often substantially reduces termination length. Our previous work employed translation to a non-generalized Büchi automaton. Though a well-known technique converts a generalized automaton into that form by composing it with a counter, it has the undesirable effect of considerably lengthening the cycles in the graph to be searched. We propose several alternatives to that approach and compare them experimentally. The translation to automata can be accomplished in more than one way, and in this paper we contrast two of them: one based on the algorithms of [F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In E. A. Emerson and A. P. Sistla, editors, Twelfth Conference on Computer Aided Verification (CAV'00), pages 248–263. Springer-Verlag, Berlin, July 2000. LNCS 1855], and one based on the notion of tight automaton of [E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In D. L. Dill, editor, Sixth Conference on Computer Aided Verification (CAV'94), pages 415–427. Springer-Verlag, Berlin, 1994. LNCS 818]. The latter yields shorter counterexamples, but the former often leads to earlier termination. In addition, it can help in identifying safety properties, for which termination checks are much more efficient than for the general case. We finally present results on comparing techniques based on cycle detection to the technique of [V. Schuppan and A. Biere. Efficient reduction of finite state model checking to reachability analysis. Software Tools for Technology Transfer, 5(2–3):185–204, Mar. 2004], which converts liveness properties into safety properties by augmentation of the model.     

Abstract Regular Tree Model Checking

Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus “satisfying”) the same bottom-up tree “predicate” languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.     

一种基于时间自动机的实时系统模型检查算法的设计与实现

该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用Visual C++语言描述了实时特性验证中的数据结构,实现了实时特性验证算法,实验表明利用该算法可以进行实时系统的形式化验证。     

任务流模型检验的研究

对任务流模型检验技术进行了讨论。任务流方法不关心状态数量、能否从一个指定状态到达另一指定状态及系统必须的状态是否存在,而是关心状态组合提供的功能是否存在及各状态组合之间是否存在指定的转换关系,从而避免了状态空间爆炸问题。模块搜索算法以模块为基础对任务流模型进行搜索来验证给定系统是否满足规范要求。     

Bytecode Verification by Model Checking

Java bytecode verification is traditionally performed by using dataflow analysis. We investigate an alternative based on reducing bytecode verification to model checking. First, we analyze the complexity and scalability of this approach. We show experimentally that, despite an exponential worst-case time complexity, model checking type-correct bytecode using an explicit-state on-the-fly model checker is feasible in practice, and we give a theoretical account why this is the case. Second, we formalize our approach using Isabelle/HOL and prove its correctness. In doing so we build on the formalization of the Java Virtual Machine and dataflow analysis framework of Pusch and Nipkow and extend it to a more general framework for reasoning about model-checking-based analysis. Overall, our work constitutes the first comprehensive investigation of the theory and practice of bytecode verification by model checking. This revised version was published online in August 2006 with corrections to the Cover Date.     

Bounded Model Checking with SNF,Alternating Automata,and Büchi Automata

Model checking of LTL formulæis traditionally carried out by a conversion to Büchi automata, and there is therefore a large body of research in this area including some recent studies on the use of alternating automata as an intermediate representation.Bounded model checking has until recently been apart from this, typically using a direct conversion from LTL to propositional logic. In this paper we give a new bounded model checking encoding using alternating automata and focus on the relationship between alternating automata and SNF. We also explore the differences in the way SNF, alternating, and Büchi automata are used from both a theoretical and an experimental perspective.     

A Stack-Slicing Algorithm for Multi-Core Model Checking

The broad availability of multi-core chips on standard desktop PCs provides strong motivation for the development of new algorithms for logic model checkers that can take advantage of the additional processing power. With a steady increase in the number of available processing cores, we would like the performance of a model checker to increase as well – ideally linearly. The new trend implies a change of focus away from cluster computers towards shared memory systems. In this paper we discuss the multi-core algorithms that are in development for the SPIN model checker.     

一种基于离散时间自动机的LTL性质检测工具

模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin.