Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning

Assume-guarantee reasoning enables a “divide-and-conquer” approach to the verification of large systems that checks system components separately while using assumptions about each component’s environment. Developing appropriate assumptions used to be a difficult and manual process. Over the past five years, we have developed a framework for performing assume-guarantee verification of systems in an incremental and fully automated fashion. The framework uses an off-the-shelf learning algorithm to compute the assumptions. The assumptions are initially approximate and become more precise by means of counterexamples obtained by model checking components separately. The framework supports different assume-guarantee rules, both symmetric and asymmetric. Moreover, we have recently introduced alphabet refinement, which extends the assumption learning process to also infer assumption alphabets. This refinement technique starts with assumption alphabets that are a subset of the minimal interface between a component and its environment, and adds actions to it as necessary until a given property is shown to hold or to be violated in the system. We have applied the learning framework to a number of case studies that show that compositional verification by learning assumptions can be significantly more scalable than non-compositional verification. J.M. Cobleigh currently employed by The MathWorks, Inc., 3 Apple Hill Drive, Natick, MA 01760, USA.     

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.     

Verification of Hierarchical State/Event Systems using Reusability and Compositionality

We investigate techniques for verifying hierarchical systems, i.e., finite state systems with a nesting capability. The straightforward way of analysing a hierarchical system is to first flatten it into an equivalent non-hierarchical system and then apply existing finite state system verification techniques. Though conceptually simple, flattening is severely punished by the hierarchical depth of a system. To alleviate this problem, we develop a technique that exploits the hierarchical structure to reuse earlier reachability checks of superstates to conclude reachability of substates. We combine the reusability technique with the successful compositional technique of J. Lind-Nielsen, H.R. Andersen, G. Behrmann, H. Hulgaard, K. Kristoffersen, and K.G. Larsen, 1998. In: Tools and Algorithms for the Construction and Analysis of Systems, Vol. 1384 of Lecture Notes in Computer Science, pp. 201–216, and investigate the combination experimentally on industrial systems and hierarchical systems generated according to our expectations to real systems. The experimental results are very encouraging: whereas a flattening approach degrades in performance with an increase in the hierarchical depth (even when applying the technique of J. Lind-Nielsen et al. (1998)), the new approach proves not only insensitive to the hierarchical depth, but even leads to improved performance as the depth increases.     

Combining formal verification and conformance testing for validating reactive systems

This paper presents a combination of verification and conformance testing techniques to support the formal validation of reactive systems. The idea is to use symbolic test selection techniques to extract subgraphs (components) from a specification, and to perform the verification on the components rather than on the whole specification. Under reasonable sufficient conditions, this constitutes a sound compositional verification technique, in the sense that a property verified on the components also holds on the whole specification. This may considerably reduce the global verification effort. Moreover, once verified, a component forms the basis of an adequate test case, i.e. when executed on an implementation, it will not issue false positive or negative verdicts with respect to the verified properties. The approach has been implemented using the STG test selection tool and the PVS theorem prover. It is demonstrated here on a smart‐card application: the Common Electronic Purse System. Copyright © 2003 John Wiley & Sons, Ltd.     

LVT: a layered verification technique for distributed computing systems

This paper presents a layered verification technique, called LVT, for the verification of distributed computing systems with multiple component layers. Each lower layer in such a system provides services in support of functionality of the higher layer. By taking a very general view of programming languages as interfaces of systems, LVT treats each layer in a distributed computing system as a distributed programming language. Each relatively higher‐level language in the computing system is implemented in terms of a lower‐level language. The verification of each layer in a distributed computing system can then be viewed as the verification of implementation correctness for a distributed language. This paper also presents the application of LVT to the verification of a distributed computing system, which has three layers: a small high‐level distributed programming language; a multiple processor architecture consisting of an instruction set and system calls for inter‐process message passing; and a network interface. Programs in the high‐level language are implemented by a compiler mapping from the language layer to the multiprocessor layer. System calls are implemented by network services. LVT and its application demonstrate that the correct execution of a distributed program, most notably its inter‐process communication, is verifiable through layers. The verified layers guarantee the correctness of (1) the compiled code that makes reference to operating system calls, (2) the operating system calls in terms of network calls, and (3) the network calls in terms of network transmission steps. The specification and verification involved are carried out by using the Cambridge Higher Order Logic (HOL) theorem proving system. Copyright © 1999 John Wiley & Sons, Ltd.     

Formal Verification of a Complex Pipelined Processor

This paper addresses the problem of formally verifying the correctness of a complex pipelined microprocessor at the micro-architectural level of abstraction. The design verified is an example out-of-order execution processor with a reorder buffer, a store buffer, branch prediction, speculative execution and exceptions. We propose a systematic approach called the Completion Functions Approach to decompose and incrementally build its proof of correctness. The central idea is to construct the abstraction function using completion functions, one per unfinished instruction, each of which specifies the effect on the programmer visible state components of completing the instruction. This construction of the abstraction function leads to a very natural decomposition of the proof into proving a series of verification conditions. The approach prescribes a systematic way to generate these verification conditions which can then be discharged with a high degree of automation using techniques based on decision procedures and rewriting. The verification was completed in 34 person days, which we believe, is a modest investment in return for the significant benefits of formal verification.     

A model-extraction approach to verifying concurrent C programs with CADP

The development of reliable software for industrial critical systems benefits from the use of formal models and verification tools for detecting and correcting errors as early as possible. Ideally, with a complete model-based methodology, the formal models should be the starting point to obtain the final reliable code and the verification step should be done over the high-level models. However, this is not the case for many projects, especially when integrating existing code. In this paper, we describe an approach to verify concurrent C code by automatically extracting a high-level formal model that is suitable for analysis with existing tools. The basic components of our approach are: (1) a method to construct a labeled transition system from the source code, that takes flow control and interaction among processes into account; (2) a modeling scheme of the behavior that is external to the program, namely the functionality provided by the operating system; (3) the use of demand-driven static analyses to make a further abstraction of the program, thus saving time and memory during its verification. The whole proposal has been implemented as an extension of the CADP toolbox, which already provides a variety of analysis modules for several input languages using labeled transition systems as the core model. The approach taken fits well within the existing architecture of CADP which does not need to be altered to enable C program verification. We illustrate the use of the extended CADP toolbox by considering examples of the VLTS benchmark suite and C implementations of various concurrent programs.     

Analysis of Timed Systems Using Time-Abstracting Bisimulations

The objective of this paper is to show how verification of dense-time systems modeled as timed automata can be effectively performed using untimed verification techniques. In that way, the existing rich infrastructure in algorithms and tools for the verification of untimed systems can be exploited. The paper completes the ideas introduced in (Tripakis and Yovine, 1996, in Proc. 8th Conf. Computer-Aided Verification, CAV'96, Rutgers, NJ. LNCS, Vol. 1102, Springer-Verlag, 1996, pp. 232–243).Our approach consists in two steps. First, given a timed system A, we compute a finite graph G which captures the behavior of A modulo the fact that exact time delays are abstracted away. Then, we apply untimed verification techniques on G to prove properties on A. As property-specification languages, we use both the linear-time formalism of timed Büchi automata (TBA) and the branching-time logic TCTL. Model checking A against properties specified as TBA or TCTL formulae comes down to applying, respectively, automata-emptiness or CTL model-checking algorithms on G.The abstraction of exact delays is formalized under the concept of time-abstracting bisimulations. We define three time-abstracting bisimulations which are strictly ordered with respect to their reduction power. The stronger of them preserves both linear- and branching-time properties whereas the two weaker ones preserve only linear-time properties.The finite graph G is the quotient A with respect to a time-abstracting bisimulation. Generating G is called minimization and can be done by adapting a partition-refinement algorithm to the timed case. The adapted algorithm is symbolic, that is, equivalence classes are represented as simple polyhedra. When these polyhedra are not convex, operations become expensive, therefore, we develop a partition-refinement technique which preserves convexity.We have implemented the minimization algorithm in a prototype module called minim, as part of the real-time verification platform KRONOS (Bozga et al., 1998, in CAV'98). minim connects KRONOS to the CADP tool suite for the verification of untimed graphs (Fernandez et al., 1992, in 14th Int. Conf. on Software Engineering). To demonstrate the practical interest behind our approach, we present two case studies, namely, Fischer's mutual exclusion protocol and the CSMA/CD communication protocol.     

Modular abstractions for verifying real-time distributed systems

In this work we present a verification methodology for real-time distributed systems, based on their modular decomposition into processes. Given a distributed system, each of its components is reduced by abstracting away from details that are irrelevant for the required specification. The abstract components are then composed to form an abstract system to which a model checking procedure is applied. The abstraction relation and the specification language guarantee that if the abstract system satisfies a specification, then the original system satisfies it as well.The specification languageRTL is a branching-time version of the real-time temporal logicTPTL presented in Alur and Henzinger [1]. Its model checking is linear in the size of the system and exponential in the size of the formula. Two notions of abstraction for real-time systems are introduced, each preserving a sublanguage ofRTL.     

On the correctness of upper layers of automotive systems

Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München.     

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.     

构件式系统的建模与验证

构件的组合与安全性是构件式系统开发的一个挑战性问题。提出了一种新的描述构件交互行为的模型-构件消息自动机,其特点是保留了构件的所有交互特性以便进一步进行构件的验证。给出了使用同步积操作将多个构件组合成单个复杂的组合构件的方法。基于监控理论的可控性概念,设计了一个验证构件系统安全性质的算法。为了说明论文建议的方法,详细讨论了一个简单的、贯穿整个论文的示例系统。     

A verification framework with application to a propulsion system

This paper introduces a novel verification framework for Prognostics and Health Management (PHM) systems. Critical aircraft, spacecraft and industrial systems are required to perform robustly, reliably and safely. They must integrate hardware and software tools intended to detect and identify incipient failures and predict the remaining useful life (RUL) of failing components. Furthermore, it is desirable that non-catastrophic faults be accommodated, that is fault tolerant or contingency management algorithms be developed that will safeguard the operational integrity of such assets for the duration of the emergency. It is imperative, therefore, that models and algorithms designed to achieve these objectives be verified before they are validated and implemented on-board an aircraft. This paper develops a verification approach that builds upon concepts from system analysis, specification definition, system modeling, and Monte Carlo simulations. The approach is implemented in a hierarchical structure at various levels from component to system safety. Salient features of the proposed methodology are illustrated through its application to a spacecraft propulsion system.     

微内核操作系统互斥量模块功能正确性的形式化验证

操作系统在许多安全攸关领域为软件系统提供关键性底层支撑，操作系统中一个微小的错误或漏洞都可能引起整个软件系统的重大故障，造成巨大经济损失或危及人身安全.为了减少此类安全事故的发生，对操作系统正确性进行验证十分必要.传统测试手段无法穷尽系统中的所有潜在错误，因而操作系统验证有必要使用具有严格数学理论基础的形式化方法.在操作系统中，互斥量可协调多任务对资源的访问，是一种常用的任务同步方式，其功能正确性对于保障多任务应用的正确性十分关键.本文基于定理证明方法，在交互式定理证明器Coq中对某抢占式微内核操作系统的互斥量模块进行代码级形式化建模，给出其接口函数的形式化规范，并实现这些接口函数的功能正确性验证.     

Local Module Checking for CTL Specifications

Model checking is a well known technique for the verification of finite state models using temporal logic specification. While model checking is suitable for transformational systems (also called closed systems), it is unsuitable for open systems (also known as reactive systems) where the nondeterminism in the environment must be considered during verification. Module checking is an approach for the verification of open systems which have both closed (internal) and open (environment or external) states. It has been demonstrated in [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. Module checking. Information and Computation, 164:322–344, 2001] that the complexity of module checking branching time logic CTL is EXPTIME-complete. The approach to module checking is global and the method tries to establish that the property in question holds over all possible environments.This papers develops a local approach to CTL module checking using tableau rules. The proposed approach tries to determine a single environment under which the negation of the property is satisfied over the given module. Such a strategy, thus, leads to a local approach to module checking where we only explore states that are relevant to proving that the negation of the property can be satisfied over the given module using an appropriate witness (environment) that the algorithm also generates. While the worst case complexity of our algorithm is identical to the earlier complexity, we demonstrate that practical implementation of the proposed approach is feasible and yields much better results than the global approach.     

Design verification in model-based?��-controller development using an abstract component

Component-based software development is a promising approach for controlling the complexity and quality of software systems. Nevertheless, recent advances in quality control techniques do not seem to keep up with the growing complexity of embedded software; embedded systems often consist of dozens to hundreds of software/hardware components that exhibit complex interaction behavior. Unanticipated quality defects in a component can be a major source of system failure. To address this issue, this paper suggests a design verification approach integrated into the model-driven, component-based development methodology Marmot. The notion of abstract components—the basic building blocks of Marmot—helps to lift the level of abstraction, facilitates high-level reuse, and reduces verification complexity by localizing verification problems between abstract components before refinement and after refinement. This enables the identification of unanticipated design errors in the early stages of development. This work introduces the Marmot methodology, presents a design verification approach in Marmot, and demonstrates its application on the development of a μ-controller-based abstraction of a car mirror control system. An application on TinyOS shows that the approach helps to reuse models as well as their verification results in the development process.     

复杂内核数据结构程序形式化验证

操作系统内核作为软件系统的基础组件, 其安全可靠是构造高可信软件系统的重要环节, 但是, 在实际的验证工作中, 操作系统内核中全局性质的不变式定义, 复杂数据结构程序的形式化描述和验证仍存在很多困难. 本文针对操作系统内核中满足的全局性质, 在代码层以函数为单位, 用全局不变式进行定义, 并在不同的函数中进行形式化验证, 从而证明各个函数符合操作系统内核的全局性质; 针对操作系统内核中经常使用的复杂数据结构程序, 本文通过扩展形状图理论, 提出一种使用嵌套形状图逻辑的方法来形式化描述复杂数据结构程序, 并对该方法进行了正确性证明, 最终成功验证操作系统内核中关于任务创建与调度, 消息队列创建与操作相关的代码.     

An approach to formal verification of human–computer interaction

The correct functioning of interactive computer systems depends on both the faultless operation of the device and correct human actions. In this paper, we focus on system malfunctions due to human actions. We present abstract principles that generate cognitively plausible human behaviour. These principles are then formalised in a higher-order logic as a generic, and so retargetable, cognitive architecture, based on results from cognitive psychology. We instantiate the generic cognitive architecture to obtain specific user models. These are then used in a series of case studies on the formal verification of simple interactive systems. By doing this, we demonstrate that our verification methodology can detect a variety of realistic, potentially erroneous actions, which emerge from the combination of a poorly designed device and cognitively plausible human behaviour.     

32位RISC微处理器FPGA验证平台设计与实现

微处理器的验证工作是一项复杂而重要的工作。针对传统的FPGA验证在板级验证过程中存在不能快速定位错误和调试方法单一等问题,同时结合“龙腾R2”微处理器的验证需求,设计了“龙腾R2”微处理器的FPGA验证平台,在该验证平台上成功进行了指令和VxWorks操作系统的测试。实践表明该验证平台大大缩短了验证周期,整个验证平台原理清晰,结构简单,扩展灵活、方便。