Eliminating synchronization faults in air traffic control software via design for verification with concurrency controllers

The increasing level of automation in critical infrastructures requires development of effective ways for finding faults in safety critical software components. Synchronization in concurrent components is especially prone to errors and, due to difficulty of exploring all thread interleavings, it is difficult to find synchronization faults. In this paper we present an experimental study demonstrating the effectiveness of model checking techniques in finding synchronization faults in safety critical software when they are combined with a design for verification approach. We based our experiments on an automated air traffic control software component called the Tactical Separation Assisted Flight Environment (TSAFE). We first reengineered TSAFE using the concurrency controller design pattern. The concurrency controller design pattern enables a modular verification strategy by decoupling the behaviors of the concurrency controllers from the behaviors of the threads that use them using interfaces specified as finite state machines. The behavior of a concurrency controller is verified with respect to arbitrary numbers of threads using the infinite state model checking techniques implemented in the Action Language Verifier (ALV). The threads which use the controller classes are checked for interface violations using the finite state model checking techniques implemented in the Java Path Finder (JPF). We present techniques for thread isolation which enables us to analyze each thread in the program separately during interface verification. We conducted two sets of experiments using these verification techniques. First, we created 40 faulty versions of TSAFE using manual fault seeding. During this exercise we also developed a classification of faults that can be found using the presented design for verification approach. Next, we generated another 100 faulty versions of TSAFE using randomly seeded faults that were created automatically based on this fault classification. We used both infinite and finite state verification techniques for finding the seeded faults. The results of our experiments demonstrate the effectiveness of the presented design for verification approach in eliminating synchronization faults.     

Automated circular assume-guarantee reasoning

Model checking is a successful approach for verifying hardware and software systems. Despite its success, the technique suffers from the state explosion problem which arises due to the large state space of real-life systems. One solution to the state explosion problem is compositional verification, that aims to decompose the verification of a large system into the more manageable verification of its components. To account for dependencies between components, assume-guarantee reasoning defines rules that break-up the global verification of a system into local verification of individual components, using assumptions about the rest of the system. In recent years, compositional techniques have gained significant successes following a breakthrough in the ability to automate assume-guarantee reasoning. However, automation has been restricted to simple acyclic assume-guarantee rules. In this work, we focus on automating circular assume-guarantee reasoning in which the verification of individual components mutually depends on each other. We use a sound and complete circular assume-guarantee rule and we describe how to automatically build the assumptions needed for using the rule. Our algorithm accumulates joint constraints on the assumptions based on (spurious) counterexamples obtained from checking the premises of the rule, and uses a SAT solver to synthesize minimal assumptions that satisfy these constraints. To the best of our knowledge, our work is the first to fully automate circular assume-guarantee reasoning. We implemented our approach and compared it with established non-circular compositional methods that use learning or SAT-based techniques. The experiments show that the assumptions generated for the circular rule are generally smaller, and on the larger examples, we obtain a significant speedup.     

一种大规模并行程序模型的检测方法

JPF是NASA开发的Java程序模型检测工具。该文通过改写JPF内核中生成状态空间的模块,使待检测程序在受监控状态下模拟执行。用Data-Race算法收集警告信息,引导程序模型检测工具只对死锁相关线程进行模型检测,避免了状态空间爆炸,实现了对大规模并行程序部分线程死锁问题的模型检测。利用启发式搜索算法,在不同的搜索深度赋给待执行线程不同的权值,进一步优化了模拟执行 结果。     

构件组合的抽象精化验证

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.     

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach

The state space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (operating respectively on data and events) within a counterexample-guided abstraction refinement (CEGAR) scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Our explicit use of compositionality delays the onset of state space explosion for as long as possible. To our knowledge, this is the first compositional use of CEGAR in the context of model checking concurrent C programs. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC.     

Model Checking Programs

The majority of work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers, proof checkers and model checkers. In this paper we will attempt to give convincing arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle big states, and partial order and symmetry reduction, slicing, abstraction, and runtime analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, runtime analysis, and slicing with model checking.     

构件式实时系统建模与验证研究

在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.     

Learning-based symbolic assume-guarantee reasoning for Markov decision process by using interval Markov process

Many real-life critical systems are described with large models and exhibit both probabilistic and non-deterministic behaviour. Verification of such systems requires techniques to avoid the state space explosion problem. Symbolic model checking and compositional verification such as assume-guarantee reasoning are two promising techniques to overcome this barrier. In this paper, we propose a probabilistic symbolic compositional verification approach (PSCV) to verify probabilistic systems where each component is a Markov decision process (MDP). PSCV starts by encoding implicitly the system components using compact data structures. To establish the symbolic compositional verification process, we propose a sound and complete symbolic assume-guarantee reasoning rule. To attain completeness of the symbolic assume-guarantee reasoning rule, we propose to model assumptions using interval MDP. In addition, we give a symbolic MTBDD-learning algorithm to generate automatically the symbolic assumptions. Moreover, we propose to use causality to generate small counterexamples in order to refine the conjecture assumptions. Experimental results suggest promising outlooks for our probabilistic symbolic compositional approach.     

基于多维度抽象和广度优先搜索空间划分的隐蔽信息流检测方法*

隐蔽信息流检测是开发可信计算机系统中的关键问题,而状态空间爆炸是基于状态机模型检测隐蔽信息流的主要障碍。提出一种多安全级系统中基于主体安全级的二维抽象方法,在此基础上设计了广度优先的搜索空间划分方法,使得划分变量的选取范围更大,扩展了搜索空间划分的应用范围,克服了深度优先划分方法中划分变量难以选取的问题。实验数据表明,结合抽象和搜索空间划分的方法有效降低了模型的验证规模,因此有效缓解了状态空间爆炸问题。     

Improving state class constructions for CTL* model checking of time Petri nets

The state space explosion is still one of the most challenging problems in formal verification using enumerative techniques. The challenge is even greater for real time systems whose state spaces are generally infinite due to time density. To use enumerative techniques with these systems, their state spaces need to be contracted into finite structures that preserve properties of interest. We propose in this paper an efficient approach to construct a contraction of the time Petri net model state space, which preserves its CTL* properties.     

A new formalism for mathematical description and verification of component-based systems

In this paper, we introduce a formal approach for composing software components into a distributed system. We describe the system as a hierarchical composition of some components, which can be distributed on a wide variety of hardware platforms and executed in parallel. We represent each component by a mathematical model and specify the abstract communication protocols of the components using Interface Automata (IAs). To model hierarchical systems, besides the basic components’ model, we will present other components, called nodes. A node consists of a set of subnodes interacting under the supervision of a controller. Each subnode, in turn, is a node or discrete event component. By considering a subnode as a node we can make hierarchical nodes/components. The entire system, therefore, forms the root of the hierarchy. A controller, in turn, is a set of subcontrollers/interface automata that specifies interaction protocol of the components inside a node. We have also presented an example demonstrating the model by illustrating nodes, subnodes, controllers, and subcontrollers. To address the state space explosion problem in system verification, we utilize the controller as a contract for independent analysis of the components and their interactions. Therefore, a node will not be analyzed directly; instead, we will analyze the controller.     

Approximate aggregation of Markovian models using alternating least squares

State based analysis of Markovian models is faced with the problem of state space explosion. To handle huge state spaces often compositional modeling and aggregation of components are used. Exact aggregation resulting in exact transient or stationary results is only possible in some cases, when the Markov process is lumpable. Therefore approximate aggregation is often applied to reduce the state space. Several approximate aggregation methods exist which are usually based on heuristics.This paper presents a new aggregation approach for Markovian components which computes aggregates that minimize the difference according to some algebraically defined function which describes the difference between the component and the aggregate. If the difference becomes zero, aggregation is exact, which means that component and aggregate are indistinguishable in the sense that transient and stationary results in any environment are identical. For the computation of aggregates, an alternating least squares approach is presented which tries to minimize the norm-wise difference between the original component and the aggregate. Algorithms to compute aggregates are also introduced and the quality of the approximation is evaluated by means of several examples.     

A practical data-flow verification scheme for business processes

Data in business processes becomes more and more important. Current standard languages for process modeling like BPMN 2.0 which include the data flow reflect this. Ensuring the correctness of the data flow in processes is challenging. Model checking, i.e., verifying properties of process models, is a well-known technique to this end. An important part of model checking is the construction of the state space of the model. However, state-space explosion typically is in the way of an effective verification. We study how to overcome this problem in our context by means of reduction. More specifically, we propose a reduction on the level of the process model. To our knowledge, this is new for the data-flow analysis of processes. The core of our approach are so-called regions of the process model that are relevant for the verification of properties describing the data flow. Non-relevant regions are candidates for reduction of the process model, yielding a smaller state space. Our evaluation shows that our approach works well on industrial process models.     

基于Petri网的工作流模型简化

计算状态空间可达图是验证工作流正确性的主要方法,状态空间爆炸是这类方法的主要困难.文章对线性时态逻辑LTL-x描述的正确性提出了一种基于Petri网图形化简的验证方法,证明了所提出化简规则的完备性,并以实例说明了所提方法的有效性.     

Component Verification with Automatically Generated Assumptions

Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work introduces an approach that brings a new dimension to model checking of software components. When checking a component against a property, our modified model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of two NASA applications.This paper is an expanded version of Giannakopoulou et al. (2002).     

时间行为协议状态空间约减算法

对复杂时间行为协议状态进行约减对于缓解形式化验证的状态空间爆炸问题,提高验证工具系统的效率、实用性等具有重要意义。分析了实时构件组合的几种形态,对基于时间行为协议的组合理论和状态空间爆炸问题进行了讨论,给出了时间行为协议的状态空间约减算法并进行了分析,给出了示例。     

A lazy approach to symmetry reduction

Symmetry reduction is a technique to counter state explosion for systems with regular structure. It relies on idealistic assumptions about indistinguishable components, which in practice may only be similar. In this article, we present a flexible, lazy approach to symmetry-reducing a structure without any prior knowledge about its global symmetry. Instead of a-priori checking for compliance with symmetry conditions, each encountered state is annotated on the fly with information about how symmetry is violated along the path leading to it. The method naturally favors “very symmetric” systems: more similarity among the components leads to greater compression. A notion of subsumption is used to prune the annotated search space during exploration. Previous solutions to the approximate symmetry reduction problem are restricted to specific types of asymmetry, such as up to bisimilarity, or incur a large overhead, either during preprocessing of the structure or during the verification run. In contrast, the strength of our method is its balance between ease of implementation and algorithmic flexibility. We include analytic and experimental results that witness its efficiency.     

一种面向攻击图的即时验证方法

攻击图将原本孤立的攻击行为关联起来,描述潜在攻击路径,是一种网络脆弱性分析技术.现有方法通常从攻击目标节点开始进行反向搜索,找出所有可能的攻击路径,从而对网络进行安全分析.本文在攻击图的基础上,提出了一种基于正向搜索的即时验证方法.该方法快速搜索网络中的一条完整攻击路径,通常只需构造网络系统的部分状态空间,从而减轻了内存不足和状态爆炸等问题,可作为已有方法的补充.实验表明本文方法具备良好的性能和可扩展性.     

Past‐Free[ze] reachability analysis: reaching further with DAG‐directed exhaustive state‐space analysis

Model‐checking enables the automated formal verification of software systems through the explicit enumeration of all the reachable states. While this technique has been successfully applied to industrial systems, it suffers from the state‐space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. In this paper, we present a new reachability analysis algorithm, named Past‐Free[ze], that reduces the state‐space explosion problem by freeing parts of the state‐space from memory. This algorithm relies on the explicit isolation of the acyclic parts of the system before analysis. The parallel composition of these parts drives the reachability analysis, the core of all model‐checkers. During the execution, the past states of the system are freed from memory making room for more future states. To enable counter‐example construction, the past states can be stored on external storage. To show the effectiveness of the approach, the algorithm was implemented in the OBP Observation Engine and was evaluated both on a synthetic benchmark and on realistic case studies from automotive and aerospace domains. The benchmark, composed of 50 test cases, shows that in average, 75% of the state‐space can be dropped from memory thus enabling the exploration of up to 14 times more states than traditional approaches. Moreover, in some cases, the reachability analysis time can be reduced by up to 25%. In realistic settings, the use of Past‐Free[ze] enabled the exploration of a state‐space 4.5 times larger on the automotive case study, where almost 50% of the states are freed from memory. Moreover, this approach offers the possibility of analyzing an arbitrary number of interactions between the environment and the system‐under‐verification; for instance, in the case of the aerospace example, 1000 pilot/system interactions could be analyzed unraveling an 80 GB state‐space using only 10 GB of memory. Copyright © 2016 John Wiley & Sons, Ltd.     

Formal Verification of a Distributed Computer System

Modeling distributed computer systems is known to be a challenging enterprise. Typically, distributed systems are comprised of large numbers of components whose coordination may require complex interactions. Modeling such systems more often than not leads to the nominal intractability of the resulting state space. Various formal methods have been proposed to address the modeling of coordination among distributed systems components. For the most part, however, these methods do not support formal verification mechanisms. By way of contrast, the L-automata/L-processes model supports formal verification mechanisms which in many examples can successfully circumvent state space explosion problems, and allow verification proofs to be extended to an arbitrary number of components. After reviewing L-automata/L-processes formalisms, we present here the formal specification of a fault-tolerant algorithm for a distributed computer system. We also expose the L-automata/L-processes verification of the distributed system, demonstrating how various techniques such as homomorphic reduction, induction, and linearization, can be used to overcome various problems which surface as one models large, complex systems.