Checking Finite Traces using Alternating Automata

We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a future linear-time temporal logic formula. The three methods are all based on alternating automata, but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. All three methods have been implemented and experimental results are presented. We outline an extension to these algorithms that is applicable to LTL formulas containing both past and future operators.     

Symbolic model checking for probabilistic timed automata

Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of probabilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.     

Tool support for learning Büchi automata and linear temporal logic

We introduce a graphical interactive tool, named GOAL, that can assist the user in understanding Büchi automata, linear temporal logic, and their relation. Büchi automata and linear temporal logic are closely related and have long served as fundamental building blocks of linear-time model checking. Understanding their relation is instrumental in discovering algorithmic solutions to model checking problems or simply in using those solutions, e.g., specifying a temporal property directly by an automaton rather than a temporal formula so that the property can be verified by an algorithm that operates on automata. One main function of the GOAL tool is translation of a temporal formula into an equivalent Büchi automaton that can be further manipulated visually. The user may edit the resulting automaton, attempting to optimize it, or simply run the automaton on some inputs to get a basic understanding of how it operates. GOAL includes a large number of translation algorithms, most of which support past temporal operators. With the option of viewing the intermediate steps of a translation, the user can quickly grasp how a translation algorithm works. The tool also provides various standard operations and tests on Büchi automata, in particular the equivalence test which is essential for checking if a hand-drawn automaton is correct in the sense that it is equivalent to some intended temporal formula or reference automaton. Several use cases are elaborated to show how these GOAL functions may be combined to facilitate the learning and teaching of Büchi automata and linear temporal logic. This work was partially supported by the National Science Council, Taiwan (R.O.C.) under grants NSC94-2213-E-002-089, NSC95-2221-E-002-127, NSC95-3114-P-001-001-Y02 (iCAST 2006), NSC96-3114-P-001-002-Y (iCAST 2007), and NSC97-2221-E-002-074-MY3.     

Practical CTL* model checking: Should SPIN be extended?

We describe an efficient CTL^* model checking algorithm based on alternating automata and games. A CTL^* formula, expressing a correctness property, is first translated to a hesitant alternating automaton and then composed with a Kripke structure representing the model to be checked, after which this resulting automaton is then checked for nonemptiness. We introduce the nonemptiness game that checks the nonemptiness of a hesitant alternating automaton (HAA). In the same way that alternating automata generalise nondeterministic automata, we show that this game for checking the nonemptiness of HAA, generalises the nested depth-first algorithm used to check the nonemptiness of nondeterministic Büchi automata (used in Spin).     

基于概率时间自动机的异构多agent自适应运行时验证

多agent自适应系统在运行过程中需要根据环境进行自适应调整。异构agent能够提高agent的使用效率和降低系统的构建成本,但存在复杂的协作问题,因此提出一种基于概率时间自动机的异构多agent自适应系统运行时验证方法。该方法通过形式化描述异构agent的功能特征并融合环境中的随机因素构建概率时间自动机模型模拟自适应系统的运行过程;针对异构agent之间的协作逻辑制定安全约束条件以确保系统运行中状态迁移流程的安全性。通过模型检查结合运行时定量验证方法进行实验验证,在智能泊车系统案例中应用该方法。实验结果表明,agent之间协作逻辑的正确性可以有效保证系统运行时的稳定性,且相较于不使用运行时定量验证的初始系统在相同时间内正常运行的时间提升了21%左右。     

Collecting Statistics Over Runtime Executions

We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of statistical data. By collecting statistics over runtime executions of a program we can answer complex queries, such as “what is the average number of packet transmissions' in a communication protocol, or “how often does a particular process enter the critical section while another process remains waiting' in a mutual exclusion algorithm. To decouple the evaluation strategy of the queries from the definition of the temporal operators, we introduce algebraic alternating automata as an automata-based intermediate representation. Algebraic alternating automata are an extension of alternating automata that produce a value instead of acceptance or rejection for each trace. Based on the translation of the formulas from the query language to algebraic alternating automata, we obtain a simple and efficient query evaluation algorithm. The approach is illustrated with examples and experimental results.     

PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

Effective synchronizing algorithms

The notion of a synchronizing sequence plays an important role in the model-based testing of reactive systems, such as sequential circuits or communication protocols. The main problem in this approach is to find the shortest possible sequence which synchronizes the automaton being a model of the system under test. This can be done with a synchronizing algorithm. In this paper we analyze the synchronizing algorithms described in the literature, both exact (with exponential runtime) and greedy (polynomial). We investigate the implementation of the exact algorithm and show how this implementation can be optimized by use of some efficient data structures. We also propose a new greedy algorithm, which relies on some new heuristics. We compare our algorithms with the existing ones, with respect to both runtime and quality aspect.     

Verifying Communication Protocols Using Live Sequence Chart Specifications

The need for a formal verification process in System on Chip (SoC) design and Intellectual Property (IP) integration has been recognized and investigated significantly in the past. A major drawback is the lack of a suitable specification language against which definitive and efficient verification of inter-core communication can be performed to prove compliance of an IP block against the protocol specification. Previous research has yielded positive results of verifying systems against the graphical language of Live Sequence Charts (LSCs) but has identified key limitations of the process that arise from the lack of support for important constructs of LSCs such as Kleene stars, subcharts, and hierarchical charts. In this paper we further investigate the use of LSCs as a specification language and show how it can be formally translated to automata suitable for input to a model checker for automatic verification of the system under test. We present the translation for subcharts, Kleene stars, and hierarchical charts that are essential for protocol specification and have not been translated to automata before. Further, we successfully translate the BVCI protocol (point to point communication protocol) specification from LSC to an automaton and present a case study of verifying models using the resulting automaton.     

Reactive automata

A reactive automaton has extra links whose role is to change the behaviour of the automaton. We show that these links do not increase the expressiveness of finite automata but that they can be used to reduce dramatically their state number both in the deterministic case and the non-deterministic case.Typical examples of regular expressions associated with deterministic automata of exponential size according to the length of the expression show that reactive links provide an alternative representation of total linear size for the language.     

Memory-efficient algorithms for the verification of temporal properties

This article addresses the problem of designing memory-efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are modeled as automata on infinite words (Büchi automata). Verification is then reduced to checking the emptiness of the automaton resulting from the product of the program and the property. This problem is usually solved by computing the strongly connected components of the graph representing the product automaton. Here, we present algorithms that solve the emptiness problem without explicitly constructing the strongly connected components of the product graph. By allowing the algorithms to err with some probability, we can implement them with a randomly accessed memory of size O(n) bits, where n is the number of states of the graph, instead of O(n log n) bits that the presently known algorithms require.     

Lower and upper bounds in zone-based abstractions of timed automata

Timed automata have an infinite semantics. For verification purposes, one usually uses zone-based abstractions w.r.t. the maximal constants to which clocks of the timed automaton are compared. We show that by distinguishing maximal lower and upper bounds, significantly coarser abstractions can be obtained. We show soundness and completeness of the new abstractions w.r.t. reachability and demonstrate how information about lower and upper bounds can be used to optimise the algorithm for bringing a difference bound matrix into normal form. Finally, we experimentally demonstrate that the new techniques dramatically increase the scalability of the real-time model checker UPPAAL.     

网构软件的资源自适应性的形式化分析与验证

针对基于构件的网构软件系统对环境资源变化的自适应性特征的可信分析与验证展开研究.具体工作包括:在网构软件的系统模型层次,使用带资源语义信息的接口自动机对软件构件的行为进行形式化建模,其包含了构件在完成特定功能的过程中对环境资源的使用特征;使用资源接口自动机网络来描述构件组装实体的组合行为;使用基于场景的UML顺序图模型来描述具有多功能的组合系统规约;分别研究了检验组合系统的所有行为是否都满足给定的资源约束以及检验指定的系统行为是否满足资源约束这两个具体问题:通过对资源自动机网络状态空间的分析,构造其相应的可达图,在此基础上给出了相应的检验资源可满足性、最小资源需求量以及检验指定功能合法性等算法.     

Resolution approach to testing compatibility of interacting automata

Conclusion The notion of compatibility of automata was proposed in [1] for formalization of requirements that must be met by interacting partial automata. Testing the compatibility of automata is of essential importance for the design of systems that interact with the environment, especially when we use declarative specificatio of the system to be designed. Under the assumptions of this article for the automaton that models the environment, partiality of the specified automaton is a source of possible incompatibility with the environment. When declarative specification is used, we can never decide in advance if the specified automaton is partial or not. Moreover, even a specification thata priori describes a completely defined automaton may be altered by the actions of the designer in the process of design (especially if these actions are incorrect) so that the specified automaton becomes partial. Therefore the initial specification, and each successive specification produced by human intervention in the design process, must be tested for compatibility with the environment. In the methodology of verification design of automata, compatibility testing is used to solve two problems: a) generating the specification of the class of all automata that satisfy the initial specification and are compatible with the specification of the environment; b) testing for correctness the designer's decisions that alter the current specification of the automaton being designed. The results of this article have led to the development of an efficient resolution procedure for testing the compatibility of automaton specification with the specification of the environment. this procedure has been implemented in the system for verification design of automata from their logical specifications. The efficiency of the developed procedure is based on the results of compatibility analysis of automata from [1] and on the restricted resolution strategy whose completeness and correctness have been proved in [2]. Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 36–50, November–December, 1994.     

An Overview of the Runtime Verification Tool Java PathExplorer

We present an overview of the Java PathExplorer runtime verification tool, in short referred to as JPAX. JPAX can monitor the execution of a Java program and check that it conforms with a set of user provided properties formulated in temporal logic. JPAX can in addition analyze the program for concurrency errors such as deadlocks and data races. The concurrency analysis requires no user provided specification. The tool facilitates automated instrumentation of a program's bytecode, which when executed will emit an event stream, the execution trace, to an observer. The observer dispatches the incoming event stream to a set of observer processes, each performing a specialized analysis, such as the temporal logic verification, the deadlock analysis and the data race analysis. Temporal logic specifications can be formulated by the user in the Maude rewriting logic, where Maude is a high-speed rewriting system for equational logic, but here extended with executable temporal logic. The Maude rewriting engine is then activated as an event driven monitoring process. Alternatively, temporal specifications can be translated into automata or algorithms that can efficiently check the event stream. JPAX can be used during program testing to gain increased information about program executions, and can potentially furthermore be applied during operation to survey safety critical systems.     

格值交替树自动机

交替（树）自动机因其本身关于取补运算的简洁性及其与非确定型（树）自动机的等价性,成为自动机与模型检测领域研究的一个新方向.在格值交替自动机与经典交替树自动机概念的基础上,引入格值交替树自动机的概念,并研究了格值交替树自动机的代数封闭性和表达能力.首先,证明了对格值交替树自动机的转移函数取对偶运算,终止权重取补之后所得自动机与原自动机接受语言互补这一结论.其次,证明了格值交替树自动机关于交、并运算的封闭性.最后,讨论了格值交替树自动机和格值树自动机、格值非确定型自动机的表达能力;证明了格值交替树自动机与格值树自动机的等价性,并给出了二者相互转化的算法及其复杂度分析;同时,提供了用格值非确定型自动机来模拟格值交替树自动机的方法.     

Recognizing malicious software behaviors with tree automata inference

We explore how formal methods and tools of the verification trade could be used for malware detection and analysis. In particular, we propose a new approach to learning and generalizing from observed malware behaviors based on tree automata inference. Our approach infers k-testable tree automata from system call dataflow dependency graphs. We show how inferred automata can be used for malware recognition and classification.     

Model checking probabilistic systems against pushdown specifications

Model checking is a fully automatic verification technique traditionally used to verify finite-state systems against regular specifications. Although regular specifications have been proven to be feasible in practice, many desirable specifications are non-regular. For instance, requirements which involve counting cannot be formalized by regular specifications but using pushdown specifications, i.e., context-free properties represented by pushdown automata. Research on model-checking techniques for pushdown specifications is, however, rare and limited to the verification of non-probabilistic systems.In this paper, we address the probabilistic model-checking problem for systems modeled by discrete-time Markov chains and specifications that are provided by deterministic pushdown automata over infinite words. We first consider finite-state Markov chains and show that the quantitative and qualitative model-checking problem is solvable via a product construction and techniques that are known for the verification of probabilistic pushdown automata. Then, we consider recursive systems modeled by probabilistic pushdown automata with an infinite-state Markov chain semantics. We first show that imposing appropriate compatibility (visibility) restrictions on the synchronizations between the pushdown automaton for the system and the specification, decidability of the probabilistic model-checking problem can be established. Finally we prove that slightly departing from this compatibility assumption leads to the undecidability of the probabilistic model-checking problem, even for qualitative properties specified by deterministic context-free specifications.     

Observation strategies for event detection with incidence on runtime verification: theory, algorithms, experimentation

Many applications (such as system and user monitoring, runtime verification, diagnosis, observation-based decision making, intention recognition) all require to detect the occurrence of an event in a system, which entails the ability to observe the system. Observation can be costly, so it makes sense to try and reduce the number of observations, without losing full certainty about the event??s actual occurrence. In this paper, we propose a formalization of this problem. We formally show that, whenever the event to be detected follows a discrete spatial or temporal pattern, then it is possible to reduce the number of observations. We discuss exact and approximate algorithms to solve the problem, and provide an experimental evaluation of them. We apply the resulting algorithms to verification of linear temporal logics formulæ. Finally, we discuss possible generalizations and extensions, and, in particular, how event detection can benefit from logic programming techniques.     

基于启发式NDFS的模型检测新算法

以带有多个可接受条件的广义Büchi自动机为研究对象,提出基于启发式NDFS的模型检测新算法.该算法结合on-the-fly算法与启发式NDFS算法,能较快地判断出广义Büchi自动机非空性,通过理论证明和实验验证了算法的正确性和可行性.与已有算法相比,在广义Büchi自动机非空的情况下,该算法减少了系统状态空间的搜索,提高了检测效率,且能形成相应反例,为缓解形式化验证中的状态空间爆炸问题提供了有效的解决途径,为安全苛求系统的安全性保障提供了有力支撑,丰富了基于模型的软件形式化开发方法.