时间自动机的LTL性质模型检测研究

为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略.采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题.与DTSpin等著名的模型检测工具进行了实验比较,取得了较好的实验结果.     

模型检测基于概率时间自动机的反例产生研究

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的κ条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.     

Model Checking Weighted Integer Reset Timed Automata

Weighted timed automata (WTA), introduced in Alur et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 49–62, Springer, Berlin, 2001), Behrmann et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 147–161, Springer, Berlin, 2001) are an extension of Alur and Dill (Theor. Comput. Sci. 126(2):183–235, 1994) timed automata, a widely accepted formalism for the modelling and verification of real time systems. Weighted timed automata extend timed automata by allowing costs on the locations and edges. There has been a lot of interest Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006), Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008), Brihaye et al. (Proceedings of FORMATS/FTRTFT’04, LNCS, vol. 3253, pp. 277–292, Springer, Berlin, 2004), Brihaye et al. (Inf. Comput. 204(3):408–433, 2006) in studying the model checking problem of weighted timed automata. The properties of interest are written using logic weighted CTL (WCTL), an extension of CTL with costs. It has been shown Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008) that the problem of model checking WTAs with a single clock using WCTL with no external cost variables is decidable, while 3 clocks render the problem undecidable Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006). The question of 2 clocks is open. In this paper, we introduce a subclass of weighted timed automata called weighted integer reset timed automata (WIRTA) and study the model checking problem. We give a clock reduction technique for WIRTA. Given a WIRTA A\mathcal{A} with n≥1 clocks, we show that a single clock WIRTA A￠\mathcal{A}' preserving the paths and costs of A\mathcal{A} can be obtained. This gives us the decidability of model checking WIRTA with n≥1 clocks and m≥1 costs using WCTL with no external cost variables. We then show that for a restricted version of WCTL with external cost variables, the model checking problem is undecidable for WIRTA with 3 stopwatch costs and 1 clock. Finally, we show that model checking WTA with 2 clocks and 1 stopwatch cost against WCTL with no external cost variables is undecidable, thereby answering a question that has remained long open.     

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

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

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.     

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

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

自动机与模型检查

首先介绍自动机识别有限词和无限词两种情况,然后结合模型检查方法,把自动机作为规范自动机与模型自动机,使用自动机识别语言的包含问题技巧来解决模型检查问题,这里强调的是Vardi与Wolper提出的方法。     

Under-approximation Heuristics for Grid-based Bounded Model Checking

In this paper, we consider the effect of BDD-based under-approximation on a hybrid approach using BDDs and SAT-BMC for error detection on a computing grid. We experimentally study effect of under-approximation approaches on a non-traditional parallelization of BMC based on state space partitioning. This parallelization is accomplished by executing multiple instances of BMC independently from different seed states, that are selected from the reachable states in different partitions. Such states are spread out across the state space and can potentially be deep. Since all processors work independently of each other, this scheme is suitable for bug hunting using a grid-like network. Our experimental results demonstrate improvement over existing approaches, and we show that the method can effectively utilize a large grid network.     

Timed Automata Patterns

Timed Automata have proven to be useful for specification and verification of real-time systems. System design using Timed Automata relies on explicit manipulation of clock variables. A number of automated analyzers for Timed Automata have been developed. However, Timed Automata lack of composable patterns for high-level system design. Logic-based specification languages like Timed CSP and TCOZ are well suited for presenting compositional models of complex real-time systems. In this work, we define a set of composable Timed Automata patterns based on hierarchical constructs in timed enriched process algebras. The patterns facilitate hierarchical design of complex systems using Timed Automata. They also allow a systematic translation from Timed CSP/TCOZ models to Timed Automata so that analyzers for Timed Automata can be used to reason about TCOZ models. A prototype has been developed to support system design using Timed Automata patterns or, if given a TCOZ specification, to automate the translation from TCOZ to Timed Automata.     

Model Checking for a Class of Weighted Automata

A large number of different model checking approaches has been proposed during the last decade. The different approaches are applicable to different model types including untimed, timed, probabilistic and stochastic models. This paper presents a new framework for model checking techniques which includes some of the known approaches and enlarges the class of models to which model checking can be applied to the general class of weighted automata. The approach allows an easy adaption of model checking to models which have not been considered yet for this purpose. Examples for those new model types for which model checking can be applied are max/plus or min/plus automata which are well established models to describe different forms of dynamic systems and optimization problems. In this context, model checking can be used to verify temporal or quantitative properties of a system. The paper first presents briefly our class of weighted automata, as a very general model type. Then Valued Computational Tree Logic (CTL) is introduced as a natural extension of the well known branching time logic CTL. Afterwards, algorithms to check a weighted automaton with respect to a CTL) is introduced as a natural extension of the well known branching time logic CTL. Afterwards, algorithms to check a weighted automaton with respect to a CTL formula are presented. As a last result, bisimulation equivalence is extended to weighted automata and CTL$.     

Timed CSP = Closed Timed Automata

We study the expressive power of an augmented version of Timed CSP and show that it is precisely equal to that of closed timed automatatimed automata with closed invariant and enabling clock constraints. We also show that this new version of Timed CSP is expressive enough to capture the most widely used specifications on timed systems as refinements between processes, and moreover that refinement checking is amenable to digitisation analysis. As a result, we are able to verify some of the most important timed specifications, including branching-time liveness properties such as timestop-freedom and constant availability, using the model checker FDR (a commercial product of Formal Systems (Europe) Ltd.).     

A Compact Linear Translation for Bounded Model Checking

We present a syntactic scheme for translating future-time LTL bounded model checking problems into propositional satisfiability problems. The scheme is similar in principle to the Separated Normal Form encoding proposed in [Frisch, A., D. Sheridan and T. Walsh, A fixpoint based encoding for bounded model checking, in: M.D. Aagaard and J.W. O'Leary, editors, Formal Methods in Computer-Aided Design; 4th International Conference, FMCAD 2002, Lecture Notes in Computer Science 2517 (2002), pp. 238–254] and extended to past time in [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)]: an initial phase involves putting LTL formulae into a normal form based on linear-time fixpoint characterisations of temporal operators.As with [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)] and [Latvala, T., A. Biere, K. Heljanko and T. Junttila, Simple bounded LTL model checking, in: Formal Methods in Computer-Aided Design; 5th International Conference, FMCAD 2004, Lecture Notes in Computer Science 3312 (2004), pp. 186–200], the size of propositional formulae produced is linear in the model checking bound, but the constant of proportionality appears to be lower.A denotational approach is taken in the presentation which is significantly more rigorous than that in [Frisch, A., D. Sheridan and T. Walsh, A fixpoint based encoding for bounded model checking, in: M.D. Aagaard and J.W. O'Leary, editors, Formal Methods in Computer-Aided Design; 4th International Conference, FMCAD 2002, Lecture Notes in Computer Science 2517 (2002), pp. 238–254] and [Cimatti, A., M. Roveri and D. Sheridan, Bounded verification of past LTL, in: A.J. Hu and A.K. Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer Aided Design (FMCAD 2004), Lecture Notes in Computer Science (2004)], and which provides an elegant alternative way of viewing fixpoint based translations in [Latvala, T., A. Biere, K. Heljanko and T. Junttila, Simple bounded LTL model checking, in: Formal Methods in Computer-Aided Design; 5th International Conference, FMCAD 2004, Lecture Notes in Computer Science 3312 (2004), pp. 186–200] and [Biere, A., A. Cimatti, E. M. Clarke, O. Strichman and Y. Zhu, Bounded model checking, Advances in Computers 58 (2003)].     

Bounded Model Checking Using Satisfiability Solving

The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.     

Bounded Model Checking for Probabilistic Computation Tree Logic

为了缓解概率计算树逻辑模型检测中的状态空间爆炸问题,提出了概率计算树逻辑的限界模型检测技术.该技术首先定义概率计算树逻辑的限界语义,并证明其正确性;之后,通过实例说明在传统限界模型检测中,以路径长度作为判断检测过程终止的标准已经失效,基于数值计算中牛顿迭代法的终止准则,设计了新的终止判断标准;然后提出基于线性方程组求解的限界模型检测算法;最后,通过3个测试用例说明,概率计算树逻辑限界模型检测方法在反例较短的情况下能够快速完成检测过程,而且比概率计算树逻辑的无界模型检测算法所需求得的状态空间要少.     

Distributed Explicit Bounded LTL Model Checking

Automated formal verification becomes a significant part of an industrial design process. Favourite formal verification method  model checking  is strongly limited by the size of the model of the verified system. It suffers from the so called state explosion problem. We propose to fight this problem by applying the idea of bounding the examined state space in explicit model checking. Moreover, we combine this approach with the distribution of the computation among the network of workstations. We consider several distributed bounded LTL model checking algorithms and carry out a series of experiments to evaluate them and to compare their behaviour.     

Computing Over-Approximations with Bounded Model Checking

Bounded Model Checking (BMC) searches for counterexamples to a property with a bounded length k. If no such counterexample is found, k is increased. This process terminates when k exceeds the completeness threshold (i.e., k is sufficiently large to ensure that no counterexample exists) or when the SAT procedure exceeds its time or memory bounds. However, the completeness threshold is too large for most practical instances or too hard to compute.Hardware designers often modify their designs for better verification and testing results. This paper presents an automated technique based on cut-point insertion to obtain an over-approximation of the model that 1) preserves safety properties and 2) has a which is small enough to actually prove using BMC. The algorithm uses proof-based abstraction refinement to remove spurious counterexamples.     

Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.     

Accelerating Bounded Model Checking of Safety Properties

Bounded Model Checking based on SAT methods has recently been introduced as a complementary technique to BDD-based Symbolic Model Checking. The basic idea is to search for a counterexample in executions whose length is bounded by some integer k. The BMC problem can be efficiently reduced to a propositional satisfiability problem, and can therefore be solved by SAT methods rather than BDDs. SAT procedures are based on general-purpose heuristics that are designed for any propositional formula. We show how the unique characteristics of BMC invariant formulas (G p) can be exploited for a variety of optimizations in the SAT checking procedure. Experiments with these optimizations on real designs prove their efficiency in many of the hard test cases, in comparison to both the standard SAT procedure and a BDD-based model checker.     

应用吴方法进行高层次定界模型检验

以吴方法为理论基础,提出一种针对高层次设计验证的定界模型检验方法.通过使用多项式等式建模高层次设计和待验证性质,将定界模型检验问题转化为定理证明问题,并用吴方法有效地解决该定理证明问题.实验结果表明,与基于布尔SAT、基于LP的RTL SAT以及基于非线性求解器的性质检验方法相比,该方法在时间消耗上具有相当大的优势.     

Spark环境下基于SMT的分布式限界模型检测

在基于可满足性模理论(SMT)的限界模型检测中,限界深度对于程序验证结果的可信性和程序验证效率具有重要影响。传统串行检测方法由于单机处理性能和内存的限制,不能在限界较深的条件下进行验证。针对该问题,在Spark环境下提出一种分布式限界模型检测方法。将源程序的LLVM中间表示(LLVM-IR)构造为Spark内置的数据结构Pair RDD,利用MapReduce算法将Pair RDD转化为表示验证条件的弹性分布式数据集(VCs RDD),VCs RDD转化为SMT-LIB并输入SMT求解器进行验证。实验结果表明,与传统串行检测方法相比,该方法提高了验证过程中的限界深度和验证结果的正确率,并且对于复杂度较高的程序在限界相同的情况下其验证速度也有所提升。