Component-wise incremental LTL model checking

Efficient symbolic and explicit-state model checking approaches have been developed for the verification of linear time temporal logic (LTL) properties. Several attempts have been made to combine the advantages of the various algorithms. Model checking LTL properties usually poses two challenges: one must compute the synchronous product of the state space and the automaton model of the desired property, then look for counterexamples that is reduced to finding strongly connected components (SCCs) in the state space of the product. In case of concurrent systems, where the phenomenon of state space explosion often prevents the successful verification, the so-called saturation algorithm has proved its efficiency in state space exploration. This paper proposes a new approach that leverages the saturation algorithm both as an iteration strategy constructing the product directly, as well as in a new fixed-point computation algorithm to find strongly connected components on-the-fly by incrementally processing the components of the model. Complementing the search for SCCs, explicit techniques and component-wise abstractions are used to prove the absence of counterexamples. The resulting on-the-fly, incremental LTL model checking algorithm proved to scale well with the size of models, as the evaluation on models of the Model Checking Contest suggests.     

Efficient approach of translating LTL formulae into Büchi automata

In explicit-state model checking, system properties are typically expressed in linear temporal logic (LTL), and translated into a Büchi automaton (BA) to be checked. In order to improve performance of the conversion algorithm, some model checkers involve the intermediate automata, such as a generalized Büchi automaton (GBA). The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions satisfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, on-the-fly degeneralization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae.We compare the conversion algorithm presented in this paper to previousworks, and show that it is more efficient for five families LTL formulae in common use and four sets of random formulae generated by LBTT (an LTL-to-Büchi translator testbench).     

RGPS过程层元模型正确性验证

利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系统实例证明该验证方法的正确性和有效性。     

Distributed breadth-first search LTL model checking

We propose a parallel distributed memory on-the-fly algorithm for enumerative LTL model checking. The algorithm is designed for networks of workstations communicating via MPI. The detection of cycles (faulty runs) effectively employs the so-called back-level edges. In particular, a parallel level synchronized breadth-first search of the graph is performed to discover all back-level edges, and for each level the back-level edges are checked in parallel by a nested search procedure to confirm or refute the presence of a cycle. Several improvements of the basic algorithm are presented and advantages and drawbacks of their application to distributed LTL model checking are discussed.Research partially supported by grant No. 1ET-408050503 and the Grant Agency of Czech Republic grant No. 201/03/0509.

---

     

Efficient approach of translating LTL formulae into Büchi automata

In explicit-state model checking, system properties are typically expressed in linear temporal logic (LTL), and translated into a Büchi automaton (BA) to be checked. In order to improve performance of the conversion algorithm, some model checkers involve the intermediate automata, such as a generalized Büchi automaton (GBA). The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions satisfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, on-the-fly degeneralization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae.We compare the conversion algorithm presented in this paper to previousworks, and show that it is more efficient for five families LTL formulae in common use and four sets of random formulae generated by LBTT (an LTL-to-Büchi translator testbench).     

基于线性时序逻辑的实时系统模型检查

模型检查是一种用于并发系统的性质验证的算法技术.LTLC(linear temporal logic with clocks)是一种连续时间时序逻辑,它是线性时序逻辑LTL的一种实时扩充.讨论实时系统关于LTLC公式的模型检查问题,将实时系统关于LTLC公式的模型检查化归为有穷状态转换系统关于LTL公式的模型检查,从而可以利用LTL的模型检查工具来对LTLC进行模型检查.由于LTLC既能表示实时系统的性质,又能表示实时系统的实现,这就使得时序逻辑LTLC的模型检查过程既能用于实时系统的性质验证,又能用于实时系统之间的一致性验证.     

ACTL strong negation and its application to hybrid systems verification

Model checking procedures for verifying properties of hybrid dynamic systems are based on the construction of finite-state abstractions. If the property is not satisfied by the abstraction, the verification is inconclusive and the abstraction needs to be refined so that a less conservative model can be checked. If the hybrid system does not satisfy the property, this verify–refine procedure usually will not terminate. This paper introduces the concept of strong negation for ACTL formulas as an auxiliary condition that can be verified to obtain a conclusive negative verification result from a finite-state abstraction in certain cases. The concepts are illustrated with an example from automotive powertrain control.     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析．应用自动机和Promela对协议进行建模。利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

A vertex centric parallel algorithm for linear temporal logic model checking in Pregel

Linear Temporal Logic (LTL) Model Checking is a very important and popular technique for the automatic verification of safety-critical hardware and software systems, aiming at ensuring their quality. However, it is well known that LTL model checking suffers from the state explosion problem, often leading to insurmountable scalability problems when applying it to real-world systems. While there has been work on distributed algorithms for explicit on-the-fly LTL model checking, these are not sufficiently scalable and capable of tolerating faults during computation, significantly limiting their usefulness in huge cluster environments. Moreover, implementing these algorithms is generally viewed as a very challenging, error-prone task. In this paper, we instead rely on Pregel, a simple yet powerful model for distributed computation on large graphs. Pregel has from the start been designed for efficient, scalable and fault tolerant operation on clusters of thousands of computers, including large cloud setups. To harness Pregel’s power, we propose a new vertex centric distributed algorithm for explicit LTL model checking of concurrent systems. Experimental results illustrate feasibility and scalability of the proposed algorithm. Compared with other distributed algorithms, our algorithm is more scalable, reliable and efficient.     

WTP协议的SPIN模型检测

基于模型检测技术,使用SPIN对WTP协议进行了建模和分析.应用自动机和Promela对协议进行建模,利用LTL规范了协议需要满足的安全性,时序性。通过分析发现了协议的一个错误。     

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System

In this work we propose a verification methodology consisting of selective quantitative timing analysis and interval model checking. Our methods can aid not only in determining if a system works correctly, but also in understanding how well the system works. The selective quantitative algorithms compute minimum and maximum delays over a selected subset of system executions. A linear-time temporal logic (LTL) formula is used to select either infinite paths or finite intervals over which the computation is performed. We show how tableau for LTL formulas can be used for selecting either paths or intervals and also for model checking formulas interpreted over paths or intervals.To demonstrate the usefulness of our methods we have verified a complex and realistic distributed real-time system. Our tool has been able to analyze the system and to compute the response time of the various components. Moreover, we have been able to identify inefficiencies that caused the response time to increase significantly (about 50%). After changing the design we not only verified that the response time was lower, but were also able to determine the causes for the poor performance of the original model using interval model checking.     

Tableau-based automata construction for dynamic linear time temporal logic*

We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.*This research has been partially supported by the project MIUR PRIN 2005 ‘Specification and verification of agent interaction protocols’.     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

Combining Local and Global Model Checking

The verification process of reactive systems in local model checking [1,7] and in explicit state model checking is[13,15] on-the-fly. Therefore only those states of a system have to be traversed that are necessary to prove a property. In addition, if the property does not hold, than often only a small subset of the state space has to be traversed to produce a counterexample. Global model checking [6,23] and, in particular, symbolic model checking [4,22] can utilize compact representations of the state space, e.g. BDDs [3], to handle much larger designs than what is possible with local and explicit model checking. We present a new model checking algorithm for LTL that combines both approaches. In essence, it is a generalization of the tableau construction of [1] that enables the use of BDDs but still is on-the-fly.     

基于关键迹和ASP的CSP模型检测

模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.     

用LTL模型检验的方法验证SpaceWire检错机制

SpaceWire是应用于航空航天领域的高速通信总线协议,对SpaceWire设计正确性与可靠性要求极高,由于传统的验证方法,存在不完备性等缺陷,对SpaceWire的严格验证一直是备受关注的问题之一。模型检验以其验证的完备性得到设计人员的重视。提出用线性时态逻辑（LTL）模型检验的方法验证SpaceWire系统的检错机制。在检错模块中,该方法与用分支时态逻辑（CTL）验证方法相比,BDD分配数和状态数明显减少,提高了验证效率,还验证了错误优先级;对检错模块处理的五种错误的发生进行验证,验证结果均为正确。该方法实现了对检错机制的完备性验证。     

CAESAR_SOLVE: A generic library for on-the-fly resolution of alternation-free Boolean equation systems

Boolean equation systems (Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems, such as equivalence checking and model checking. These problems can be solved on the fly (i.e., without constructing explicitly the state space of the system under analysis) by using a demand-driven construction and resolution of the corresponding Bes. In this article, we present a generic software library dedicated to on-the-fly resolution of alternation-free Bess. Four resolution algorithms are currently provided by the library: algorithms A1 and A2 are general, the latter being optimized to produce small-depth diagnostics, whereas algorithms A3 and A4 are specialized for handling acyclic and disjunctive/conjunctive Bess in a memory-efficient way. The library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment and is currently used for three purposes: on-the-fly equivalence checking modulo five widely used equivalence relations, on-the-fly model checking of regular alternation-free modal μ-calculus, and on-the-fly reduction of state spaces based on τ-confluence .     

Model checking Duration Calculus: a practical approach

Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).     

Improved Bounded Model Checking for the Universal Fragment of CTL

SAT-based bounded model checking (BMC) has been introduced as a complementary technique to BDD-based symbolic model checking in recent years, and a lot of successful work has been done in this direction. The approach was first introduced by A. Biere et al. in checking linear temporal logic (LTL) formulae and then also adapted to check formulae of the universal fragment of computation tree logic (ACTL) by W. Penczek et al. As the efficiency of model checking is still an important issue, we present an impr...     

LTL概率模型检验工具的实现与优化

概率模型检验建立在非概率模型检验技术的基础上,不仅能够对系统进行定性的验证,还能够定量判断系统满足相关性质的概率,具有广泛的适用性。LTL概率模型检验算法的复杂度较高,达到双重指数级别,现有的工具如PRISM与MRMC均不支持对LTL性质的验证。针对这个问题,通过对原有的LTL概率模型检验算法进行优化,实现了一个高效的LTL概率模型检验工具。通过对比实验验证了该工具的有效性。