Automated structural analysis of SCR‐style software requirements specifications using PVS

The importance of effective requirements analysis techniques cannot be overemphasized when developing software requiring high levels of assurance. Requirements analysis can be largely classified as either structural or functional. The former investigates whether definitions and uses of variables and functions are consistent, while the latter addresses whether requirements accurately reflect users' needs. Verification of structural properties for large and complex software requirements is often repetitive, especially if requirements are subject to frequent changes. While inspection has been successfully applied to many industrial applications, the authors found inspection to be ineffective when reviewing requirements to find errors violating structural properties. Moreover, current tools used in requirements engineering provide only limited support in automatically enforcing structural correctness of the requirements. Such experience has motivated research to automate straightforward but tedious activities. This paper demonstrates that a theorem prover, PVS (Prototype Verification System), is useful in automatically verifying structural correctness of software requirements specifications written in SCR (Software Cost Reduction)‐style. Requirements are automatically translated into a semantically equivalent PVS specification. Users need not be experts in formal methods or power users of PVS. Structural properties to be proved are expressed in PVS theorems, and the PVS proof commands are used to carry out the proof automatically. Since these properties are application independent, the same verification procedure can be applied to requirements of various software systems. Copyright © 2001 John Wiley & Sons, Ltd.     

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

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

Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level Synthesis

This paper presents a formal specification and a proof of correctness for the widely-used Force-Directed List Scheduling (FDLS) algorithm for resource-constrained scheduling of data flow graphs in high-level synthesis systems. The proof effort is conducted using a higher-order logic theorem prover. During the proof effort many interesting properties of the FDLS algorithm are discovered. These properties are formally stated and proved in a higher-order logic theorem proving environment. These properties constitute a detailed set of formal assertions and invariants that should hold at various steps in the FDLS algorithm. They are then inserted as programming assertions in the implementation of the FDLS algorithm in a production-strength high-level synthesis system. When turned on, the programming assertions (1) certify whether a specific run of the FDLS algorithm produced correct schedules and, (2) in the event of failure, help discover and isolate programming errors in the FDLS implementation.We present a detailed example and several experiments to demonstrate the effectiveness of these assertions in discovering and isolating errors. Based on this experience, we discuss the role of the formal theorem proving exercise in developing a useful set of assertions for embedding in the scheduler code and argue that in the absence of such a formal proof checking effort, discovering such a useful set of assertions would have been an arduous if not impossible task.     

The notion of proof in hardware verification

Recent advances in the field of hardware verification have raised some fresh (and some familiar) issues concerning the scope and limitations of formal proof. In this article, we discuss in detail some of these issues. We focus particularly on which aspects of hardware and software one can verify, in contrast to the claims that are sometimes made in that regard. Since we consider verification to be one of the more important and promising applications of automated theorem proving — our research has been concerned with this application for a number of years — a precise understanding of verification must be addressed. Although the context for our discussion is the Viper verification project, our remarks apply generally. Viper is a microprocessor designed by W. J. Cullyer, C. Pygott, and J. Kershaw of the Royal Signals and Radar Establishment of the U.K. Ministry of Defence, for use in safety-critical applications. Much to their credit, the designers intended from the start that Viper be formally verified; they presented Viper's more abstract specifications in a language suitable for formal reasoning, and they placed the design in the public domain. Since Viper microprocessors are currently being marketed as verified chips, the need exists to identify precisely to what extent verification is possible. The formal proof aspects of the verification work have been carried out at the Computer Laboratory of the University of Cambridge. To date, some important properties of a register-transfer level model of Viper, relative to a more abstract functional specification, have been proved (by the author) using the HOL proof generating system. Verified systems such as Viper seem likely to become commonplace in the near future. While proofs about the abstract models of such systems are obviously a vital contribution to our trust in them, it is also important (not least in safety-critical applications) that the limitations of the approach be understood.     

Introduction to formal methods of software design

The potential benefits of using formal methods in the design of software are discussed. Concepts are illustrated by several small examples, with the objective of helping to bridge the gap between theory and practice. The paper introduces and explains some of the terminology, symbols and notation for the discrete mathematics used in the formal methods literature, intended to assist the reader in further study.     

Automated formal analysis and verification: an overview

This paper provides an overview of various existing approaches to automated formal analysis and verification. The most space is devoted to the approach of model checking, including its basic principles as well as the different techniques that have been proposed for dealing with the state space explosion problem in model checking. This paper, however, includes a brief discussion of theorem proving and static analysis too. All of the discussed approaches are introduced mostly on an informal level, with an attempt to provide the reader with their basic ideas and references to works where more details can be found.     

A Mechanized Proof Environment for the Convenient Computations Proof Method

A mechanized verification environment made up of theories over the deductive mechanized theorem prover PVS is presented, which allows taking advantage of the convenient computations method. This method reduces the conceptual difficulty of proving a given property for all the possible computations of a system by separating two different concerns: (1) proving that special convenient computations satisfy the property, and (2) proving that every computation is related to a convenient one by a relation which preserves the property. The approach is especially appropriate for applications in which the first concern is trivial once the second has been shown, e.g., where the specification itself is that every computation reduces to a convenient one. Two examples are the serializability of transactions in distributed databases, and sequential consistency of distributed shared memories. To reduce the repetition of effort, a clear separation is made between infrastructural theories to be supplied as a proof environment PVS library to users, and the specification and proof of particular examples. The provided infrastructure formally defines the method in its most general way. It also defines a computation model and a reduction relation—the equivalence of computations that differ only in the order of finitely many independent operations. One way to prove that this relation holds between every computation and some convenient one involves the definition of a measure function from computations into a well-founded set. Two possible default measures, which can be applied in many cases, are also defined in the infrastructure, along with useful lemmas that assist in their usage. We show how the proof environment can be used, by a step-by-step explanation of an application example.     

运用定理证明的形式化方法验证SpaceWire编码电路

我国空间太阳望远镜(SST)项目采用了SpaceWire作为传输总线,目前针对SpaceWire总线的验证主要采用测试和模拟等传统的方法,这类验证方法是不完备的.本文旨在对SST项目中SpaceWire总线的DS编码电路是否如实地实现标准中的规范要求进行验证,运用定理证明的形式化方法,在HOL4工具上对该电路的设计实现与规范要求的一致性进行验证,克服了传统验证方法的局限性.     

Proving Approximate Implementations for Probabilistic I/O Automata

In this paper we introduce the notion of approximate implementations for Probabilistic I/O Automata (PIOA) and develop methods for proving such relationships. We employ a task structure on the locally controlled actions and a task scheduler to resolve nondeterminism. The interaction between a scheduler and an automaton gives rise to a trace distribution—a probability distribution over the set of traces. We define a PIOA to be a (discounted) approximate implementation of another PIOA if the set of trace distributions produced by the first is close to that of the latter, where closeness is measured by the (resp. discounted) uniform metric over trace distributions. We propose simulation functions for proving approximate implementations corresponding to each of the above types of approximate implementation relations. Since our notion of similarity of traces is based on a metric on trace distributions, we do not require the state spaces nor the space of external actions of the automata to be metric spaces. We discuss applications of approximate implementations to verification of probabilistic safety and termination.     

Formal Verification of Square Root Algorithms

We discuss the formal verification of some low-level mathematical software for the Intel® Itanium® architecture. A number of important algorithms have been proven correct using the HOL Light theorem prover. After briefly surveying some of our formal verification work, we discuss in more detail the verification of a square root algorithm, which helps to illustrate why some features of HOL Light, in particular programmability, make it especially suitable for these applications.     

Validation of HOL Proofs by Proof Checking

Formal proofs generated by mechanised theorem proving systems may consist of a large number of inferences. As these theorem proving systems are usually very complex, it is extremely difficult if not impossible to formally verify them. This calls for an independent means of ensuring the consistency of mechanically generated proofs. This paper describes a method of recording HOL proofs in terms of a sequence of applications of inference rules. The recorded proofs can then be checked by an independent proof checker. Also described in this paper is an implementation of a proof checker which is able to check a practical proof consisting of thousands of inference steps.     

Web应用中数据库交互行为验证

采用定理证明和逆向工程的方法,对Web应用中的数据库交互行为进行验证。使用Z规格说明描述需求模型,根据数据库交互的源代码和转换规则得到实现模型。从实现模型中获取Web应用的相关性质,通过Z/EVES定理证明器验证这些性质是否在需求模型的 Z规格说明中得到满足。在此基础上,设计该方法的验证框架,并开发相应的原型系统。通过图书馆数据库管理系统实例证明该方法的有 效性。     

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function

We present a new technique for verification of complex hardware devices that allows both generality and a high degree of automation. The technique is based on our new way of constructing a light-weight completion function together with new encoding of uninterpreted functions called reference file representation.Our technique combines our completion function method and reference file representation with compositional model checking and theorem proving. This extends the state of the art in two directions. First, we obtain a more general verification methodology. Second, it is easier to use, since it has a higher degree of automation.As a benchmark, we take Tomasulo's algorithm for scheduling out-of-order instruction execution used in many modern superscalar processors like the Pentium-II and the PowerPC 604. The algorithm is parameterized by the processor configuration, and our approach allows us to prove its correctness in general, independent of any actual design.     

Bounded model checking of C++ programs based on the Qt cross‐platform framework

The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, technology companies tend to invest in fast and automatic verification mechanisms, to create robust systems and reduce product recall rates. In addition, further development‐time reduction and system robustness can be achieved through cross‐platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present paper proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), known as the Efficient SMT‐based Context‐Bounded Model Checker, for verifying actual Qt‐based applications, with a success rate of 89%, for the developed benchmark suite. Furthermore, the simplified version of the Qt framework, named as Qt Operational Model, was also evaluated using other state‐of‐the‐art verifiers for C++ programs. In fact, Qt Operational Model was combined with 2 different verification approaches: explicit‐state model checking and also symbolic (bounded) model checking, during the experimental evaluation, which highlights its flexibility. The proposed methodology is the first one to formally verify Qt‐based applications, which has the potential to devise new directions for software verification of portable code.     

Efficient Simulation of Formal Processor Models

Computer systems under development are routinely modeled by simulators, and formal verification can be integrated into conventional computer system development by reasoning directly about such simulators. Simulators must be extremely fast to be usable in a real development effort. We have crafted a model for a simple processor in the logic of the ACL2 theorem prover that supports both formal analysis and efficient execution, with performance near that of a simulator written in C. We demonstrate our approach using this simple model and indicate how we applied it to our latest microprocessor.     

混成系统形式化验证

混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.     

Formal Verification of Out-of-Order Execution with Incremental Flushing

We present an approach for formally verifying that a high-level microprocessor model behaves as defined by an instruction-set architecture. The technique is based on a specialization of self consistency called incremental flushing and reduces the need and effort required to create manually-generated implementation abstractions. Additionally, incremental flushing reduces the computational complexity of the proof obligations generated when reasoning about out-of-order execution. This is accomplished by comparing the functional behavior of the implementation abstraction over two sets of inputs: one that represents normal operation and one that is simpler, but functionally equivalent. The approach is illustrated on a simple out-of-order microprocessor core.     

Towards automatic software model checking of thousands of Linux modules—a case study with Avinux

Modular software model checking of large real‐world systems is known to require extensive manual effort in environment modelling and preparing source code for model checking. Avinux is a tool chain that facilitates the automatic analysis of Linux and especially of Linux device drivers. The tool chain is implemented as a plugin for the Eclipse IDE, using the source code bounded model checker CBMC as its backend. Avinux supports a verification process for Linux that is built upon specification annotations with SLICx (an extension of the SLIC language), automatic data environment creation, source code transformation and simplification, and the invocation of the verification backend. In this paper technical details of the verification process are presented: Using Avinux on thousands of drivers from various Linux versions led to the discovery of six new errors. In these experiments, Avinux also reduced the immense overhead of manual code preprocessing that other projects incurred. Copyright © 2008 John Wiley & Sons, Ltd.     

基于SAT的软件验证

线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.     

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.