Philosophical aspects of program verification

A debate over the theoretical capabilities of formal methods in computer science has raged for more than two years now. The function of this paper is to summarize the key elements of this debate and to respond to important criticisms others have advanced by placing these issues within a broader context of philosophical considerations about the nature of hardware and of software and about the kinds of knowledge that we have the capacity to acquire concerning their performance.     

Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.     

Automated verification of pointer programs in pointer logic

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic-Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool-plcc was implemented to automatically verify a number of non-trivial pointer programs.     

Modelling and verification of delay-insensitive circuits using CCS and the Concurrency Workbench

The modelling of delay-insensitive asynchronous circuits in the process calculus CCS is addressed. MUST-testing (rather than bisimulation) is found to support verification both of the property of delay-insensitivity and of design by stepwise refinement. Automated verification is possible with a well-known tool, the Edinburgh Concurrency Workbench.     

A pragmatic proposal for the improvement of program modularity and reliability

Thedomain concept-discussed in an earlier paper-is essentially no more than a generalization of the classical operating system monitor. It is argued that domain machines may be put into immediate practical use in order to further and enhance the modularity and reliability of general software. By providing an arbitrary number of monitor-like protective structures, the monitor's proven advantages of database protection and controlled procedure entry points may be applied-within the domain machine's run-time environment-at a much finer level of modular resolution. Examples are given to demonstrate the domain architecture's ability to interdict (and intercept!) various software error conditions. It is suggested that in view of present economic realities (increasingly expensive software, ever less expensive hardware), the potential improvement of software quality through use of a more sophisticated hardware base may be worth considering by the industry.This paper is a statement of the author's personal position, which is not necessarily that of Digital Equipment Corporation. It may not be construed to imply any product commitment by Digital Equipment Corporation.     

On the Role of Metadata in Visual Language Reuse and Reverse Engineering – An Industrial Case

Collecting metadata on a family of programs is useful not only for generating statistical data on the programs but also for future re-engineering and reuse purposes. In this paper we discuss an industrial case where a project library is used to store visual programs and a database to store the metadata on these programs. The visual language in question is a domain-specific language, Function Block Language (FBL) that is used in Metso Automation for writing automation control programs. For reuse, program analysis and re-engineering activities and various data and program analysis methods are applied to study the FBL programs. Metadata stored in a database is used to provide advanced program analysis support; from the large amount of programs, the metadata allows focusing the analysis to certain kinds of programs. In this paper, we discuss the role and usage of the metadata in program analysis techniques applied to FBL programs.     

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.     

Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

This paper presents some results of integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems. The intention of this research is to use predicate transition nets as a specification method and to use first order temporal logic as a verification method so that their strengths — the easy comprehension of predicate transition nets and the reasoning power of first order temporal logic can be combined. In this paper, a theoretical relationship between the computation models of these two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; and a special temporal refutation proof technique is proposed and illustrated in verifying various concurrent properties of the predicate transition net specification of the five dining philosophers problem.     

Application of BDDs in Boolean matching techniques for formal logic combinational verification

Verifying that an implementation of a combinational circuit meets its golden specification is an important step in the design process. As inputs and outputs can be swapped by synthesis tools or by interaction of the designer, the correspondence between the inputs and the outputs of the synthesized circuit and the inputs and the outputs of the golden specification has to be restored before checking equivalence. In this paper, we review the main approaches to this isomorphism problem and show how to apply OBDDs in order to obtain efficient methods. Published online: 15 May 2001     

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.     

On the detection of communication-related errors in concurrent programs

PMD is a framework for the detection of communication-related errors in concurrent programs using post-mortem analysis. It employs a static analysis of the source code to build a model of the program, which is dynamically enhanced with crucial run-time information from a dedicated hardware monitor. The notion of Region of Channel Usage (RCU) is introduced for detecting these errors efficiently. PMD is sufficiently general-purpose to handle a variety of concurrent programming languages, such as Occam2 and Joyce.     

The effective use of the one-class SVM classifier for handwritten signature verification based on writer-independent parameters

The limited number of writers and genuine signatures constitutes the main problem for designing a robust Handwritten Signature Verification System (HSVS). We propose, in this paper, the use of One-Class Support Vector Machine (OC-SVM) based on writer-independent parameters, which takes into consideration only genuine signatures and when forgery signatures are lack as counterexamples for designing the HSVS. The OC-SVM is effective when large samples are available for providing an accurate classification. However, available handwritten signature samples are often reduced and therefore the OC-SVM generates an inaccurate training and the classification is not well performed. In order to reduce the misclassification, we propose a modification of decision function used in the OC-SVM by adjusting carefully the optimal threshold through combining different distances used into the OC-SVM kernel. Experimental results conducted on CEDAR and GPDS handwritten signature datasets show the effective use of the proposed system comparatively to the state of the art.     

图形处理中投影变换的硬件设计与验证

描述了基于浮点处理单元的投影变换的硬件实现。以提高速度为设计目标,采用Verilog语言进行设计和实现,使用ISE进行逻辑综合,并用SystemVerilog进行建模验证。结果表明,本设计极大地提高了图形处理的速度。     

基于网络芯片功能验证效率的探析

讨论了分配问题匈牙利法在网络芯片功能验证中的应用,在建立了网络芯片模型的基础上提出验证需求,针对网络芯片验证的实际问题对匈牙利法进行了扩展和改进,提出了适应于分级流水芯片提高其功能验证效率的有效方式,改进后的匈牙利法具有更好的适用性。芯片验证结果证明了其可行性及其优越性。     

The RISC ProofNavigator: a proving assistant for program verification in the classroom

This paper gives an overview of the RISC ProofNavigator, an interactive proving assistant for the area of program verification. The assistant combines the user-guided top-down decomposition of proofs with the automatic simplification and closing of proof states by an external satisfiability solver. The software exhibits a modern graphical user interface which has been developed with a focus on simplicity in order to make the software suitable for educational scenarios. Nevertheless, some use cases of a certain level of complexity demonstrate that it may be also appropriate for various realistic applications. D. A. Duce, J. Oliveira, P. Boca and R. Boute     

The use of combinators in translating a purely functional language to low-level data-flow graphs

FCL is a higher-order functional programming language which consolidates and extends a number of desirable features of existing languages. This paper describes the salient features of FCL and an algorithm for translation to highly parallel data flow graphs. The translation algorithm is based on a set of extended “combinators”. The relationship between functional programming languages and demand-driven or data-driven data flow architectures is established.     

Semantic Issues in the Verification of Agent Communication Languages

This article examines the issue of developing semantics for agent communication languages. In particular, it considers the problem of giving a verifiable semantics for such languages—a semantics where conformance (or otherwise) to the semantics could be determined by an independent observer. These problems are precisely defined in an abstract formal framework. Using this framework, a number of example agent communication frameworks are defined. A discussion is then presented, of the various options open to designers of agent communication languages, with respect the problem of verifying conformance.