Combining Software and Hardware Verification Techniques

Combining verification methods developed separately for software and hardware is motivated by the industry's need for a technology that would make formal verification of realistic software/hardware co-designs practical. We focus on techniques that have proved successful in each of the two domains: BDD-based symbolic model checking for hardware verification and partial order reduction for the verification of concurrent software programs. In this paper, we first suggest a modification of partial order reduction, allowing its combination with any BDD-based verification tool, and then describe a co-verification methodology developed using these techniques jointly. Our experimental results demonstrate the efficiency of this combined verification technique, and suggest that for moderate–size systems the method is ready for industrial application.     

Model Checking at IBM

Over the past nine years, the Formal Methods Group at the IBM Haifa Research Laboratory has made steady progress in developing tools and techniques that make the power of model checking accessible to the community of hardware designers and verification engineers, to the point where it has become an integral part of the design cycle of many teams. We discuss our approach to the problem of integrating formal methods into an industrial design cycle, and point out those techniques which we have found to be especially effective in an industrial setting.     

基于模型检测的硬件木马检测技术研究

硬件木马对原始电路的恶意篡改，已成为集成电路面临的核心安全威胁。为了保障集成电路的安全可信，研究人员提出了诸多硬件木马检测方法。其中，模型检测作为一种形式化验证方法，在设计阶段可有效检测出硬件木马。首先，阐述了模型检测的工作原理和应用流程；其次，介绍了基于模型检测的硬件木马检测技术的研究进展；最后，指出了当前该技术所面临的瓶颈，并讨论了潜在的研究方向。     

The hidden models of model checking

In the past, applying formal analysis, such as model checking, to industrial problems required a team of formal methods experts and a great deal of effort. Model checking has become popular, because model checkers have evolved to allow domain-experts, who lack model checking expertise, to analyze their systems. What made this shift possible and what roles did models play in this? That is the main question we consider here. We survey approaches that transform domain-specific input models into alternative forms that are invisible to the user and which are amenable to model checking using existing techniques—we refer to these as hidden models. We observe that keeping these models hidden from the user is in fact paramount to the success of the domain-specific model checker. We illustrate the value of hidden models by surveying successful examples of their use in different areas of model checking (hardware and software) and how a lack of suitable models hamper a new area (biological systems).     

Safety-critical systems built with COTS

In the rail transportation industry competitive pressure has led to the increased use of COTS (commercial off-the-shelf equipment in safety critical systems), making it imperative that we extend proven safety techniques to COTS based systems as well. To this end, we have developed the Vital Framework (V-Frame), which is used to develop a safety critical platform from COTS hardware and software. The key technologies in this framework are formal methods, information redundancy, a proprietary data format, and a concurrent checking scheme. Combining these technologies results in a real time, checkable correctness criterion that is a signature of the application's algorithm structure and is independent of both the hardware and the operating system. V-Frame's most significant attribute is that the fail safe properties of applications do not require the firmware to be correct: the application will operate in a fail safe (or vital) manner even if there are design faults in the operating system and/or the hardware fails. This does not mean that the application does not have to be correctly specified and designed. Formal methods are appropriate in the design of safety critical COTS systems because a generic processing environment is analogous to a formal system: it is designed to apply well defined transformation rules to inputs     

Using partial-order methods in the formal validation of industrialconcurrent programs

Formal validation is a powerful technique for automatically checking that a collection of communicating processes is free from concurrency-related errors. Although validation tools invariably find subtle errors that were missed during thorough simulation and testing, the brute-force search they perform can result in excessive memory usage and extremely long running times. Recently, a number of researchers have been investigating techniques known as partial-order methods that can significantly reduce the computational resources needed for formal validation by avoiding redundant exploration of execution scenarios. This paper investigates the behavior of partial-order methods in an industrial setting. We describe the design of a partial-order algorithm or a formal validation tool that has been used on several projects that are developing software for the Lucent Technologies 5ESS/sup (R/) telephone switching system. We demonstrate the effectiveness of the algorithm by presenting the results of experiments with actual industrial examples drawn from a variety of 5ESS application domains     

An automated verification method for distributed systems softwarebased on model extraction

Software verification methods are used only sparingly in industrial software development today. The most successful methods are based on the use of model checking. There are, however, many hurdles to overcome before the use of model checking tools can truly become mainstream. To use a model checker, the user must first define a formal model of the application, and to do so requires specialized knowledge of both the application and of model checking techniques. For larger applications, the effort to manually construct a formal model can take a considerable investment of time and expertise, which can rarely be afforded. Worse, it is hard to secure that a manually constructed model can keep pace with the typical software application, as it evolves from the concept stage to the product stage. We describe a verification method that requires far less specialized knowledge in model construction. It allows us to extract models mechanically from source code. The model construction process now becomes easily repeatable, as the application itself continues to evolve. Once the model is constructed, existing model checking techniques allow us to perform all checks in a mechanical fashion, achieving nearly complete automation. The level of thoroughness that can be achieved with this new type of software testing is significantly greater than for conventional techniques. We report on the application of this method in the verification of the call processing software for a new telephone switch that was developed at Lucent Technologies     

Scientific Theories of Computational Systems in Model Checking

Model checking, a prominent formal method used to predict and explain the behaviour of software and hardware systems, is examined on the basis of reflective work in the philosophy of science concerning the ontology of scientific theories and model-based reasoning. The empirical theories of computational systems that model checking techniques enable one to build are identified, in the light of the semantic conception of scientific theories, with families of models that are interconnected by simulation relations. And the mappings between these scientific theories and computational systems in their scope are analyzed in terms of suitable specializations of the notions of model of experiment and model of data. Furthermore, the extensively mechanized character of model-based reasoning in model checking is highlighted by a comparison with proof procedures adopted by other formal methods in computer science. Finally, potential epistemic benefits flowing from the application of model checking in other areas of scientific inquiry are emphasized in the context of computer simulation studies of biological information processing.     

Error Diagnosis in Equivalence Checking of High Performance Microprocessors

We describe techniques for diagnosing errors in formal equivalence checking of RTL and transistor level models of high performance microprocessors at Freescale Semiconductor Inc. We use Symbolic Trajectory based Evalaution (STE) for combinational equivalence checking. STE accurately captures transistor level behaviors. We use simulation based error diagnosis techniques and present a seamless integration of them in our current verification environments.     

Silicon Debug of a PowerPC™ Microprocessor Using Model Checking

When silicon is available, newly designed microprocessors are tested in specially equipped hardware laboratories, where real applications can be run at hardware speeds. However, the large volumes of code being run, plus the limited access to the internal nodes of the chip, make it very difficult to characterize the nature of any failures that occur.In this paper, we describe how temporal logic model checking was used to quickly characterize a design error exhibited during hardware testing of a PowerPC microprocessor. We outline the conditions under which model checking can efficiently characterize such failures, and show how the particular error we detected could have been revealed early in the design cycle, by model checking a short and simple correctness specification. We discuss the implications of this for verification methodologies over the full design cycle.     

Java-MaC: A Run-time Assurance Tool for Java Programs

We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance about the correct execution of target programs at run-time. Monitoring and checking is performed based on a formal specification of system requirements. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which only partially validates an implementation. Java-MaC provides a lightweight formal method solution as a viable complement to the current heavyweight formal methods. An important aspect of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors against a formal requirements specification. Another salient feature is automatic instrumentation of executable codes. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.     

An environment for formal verification based on symbolic computations

We present an environment for formally verifying hardware, based on symbolic computations. This includes a new concurrency model, called the combinational/sequential or C/S concurrency model which has close ties to hardware. We allow fairness constraints and describe methods for specifying them and for formally verifying in their presence. Properties are specified by either CTL formulae or edge-Rabin automata. We give algorithms, in the presence of fairness constraints, for model checking CTL or for checking that the language of our system is contained in the language of a property automation. Finally, techniques are given for hierarchical verification and for detecting errors quickly (early failure detection).     

Java-MaC: A Run-Time Assurance Approach for Java Programs

We describe Java-MaC, a prototype implementation of the Monitoring and Checking (MaC) architecture for Java programs. The MaC architecture provides assurance that the target program is running correctly with respect to a formal requirements specification by monitoring and checking the execution of the target program at run-time. MaC bridges the gap between formal verification, which ensures the correctness of a design rather than an implementation, and testing, which does not provide formal guarantees about the correctness of the system.Use of formal requirement specifications in run-time monitoring and checking is the salient aspect of the MaC architecture. MaC is a lightweight formal method solution which works as a viable complement to the current heavyweight formal methods. In addition, analysis processes of the architecture including instrumentation of the target program, monitoring, and checking are performed fully automatically without human direction, which increases the accuracy of the analysis. Another important feature of the architecture is the clear separation between monitoring implementation-dependent low-level behaviors and checking high-level behaviors, which allows the reuse of a high-level requirement specification even when the target program implementation changes. Furthermore, this separation makes the architecture modular and allows the flexibility of incorporating third party tools into the architecture. The paper presents an overview of the MaC architecture and a prototype implementation Java-MaC.     

General test result checking with log file analysis

We describe and apply a lightweight formal method for checking test results. The method assumes that the software under test writes a text log file; this log file is then analyzed by a program to see if it reveals failures. We suggest a state-machine-based formalism for specifying the log file analyzer programs and describe a language and implementation based on that formalism. We report on empirical studies of the application of log file analysis to random testing of units. We describe the results of experiments done to compare the performance and effectiveness of random unit testing with coverage checking and log file analysis to other unit testing procedures. The experiments suggest that writing a formal log file analyzer and using random testing is competitive with other formal and informal methods for unit testing.     

移动支付协议PCMS的形式化分析和验证

移动电子商务协议的形式化分析和验证是近年来移动电子商务协议的一个重要研究热点。以一个支付网关为中心的匿名的移动电子商务支付协议PCMS为研究对象,建立了PCMS协议的时间自动机模型,并用计算树逻辑CTL公式描述PCMS协议的部分性质,最后利用模型检测工具UPPAAL对PCMS协议的无死锁、时效性、有效性和钱原子性进行检测验证。验证结果表明,以支付网关为中心的匿名的安全支付协议PCMS满足无死锁、时效性、有效性和钱原子性。     

Automatic analysis of consistency between requirements and designs

Writing requirements in a formal notation permits automatic assessment of such properties as ambiguity, consistency, and completeness. However, verifying that the properties expressed in requirements are preserved in other software life cycle artifacts remains difficult. The existing techniques either require substantial manual effort and skill or suffer from exponential explosion of the number of states in the generated state spaces. “Light-weight” formal methods is an approach to achieve scalability in fully automatic verification by checking an abstraction of the system for only certain properties. We describe light-weight techniques for automatic analysis of consistency between software requirements (expressed in SCR) and detailed designs in low-degree-polynomial time, achieved at the expense of using imprecise data-flow analysis techniques. A specification language SCR describes the systems as state machines with event-driven transitions. We define detailed designs to be consistent with their SCR requirements if they contain exactly the same transitions. We have developed a language for specifying detailed designs, an analysis technique to create a model of a design through data-flow analysis of the language constructs, and a method to automatically generate and check properties derived from requirements to ensure a design's consistency with them. These ideas are implemented in a tool named CORD, which we used to uncover errors in designs of some existing systems     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。