Improved verification of hardware designs through antecedent conditioned slicing

Static slicing has shown itself to be a valuable tool, facilitating the verification of hardware designs. In this paper, we present a sharpened notion, antecedent conditioned slicing that provides a more effective abstraction for reducing the size of the state space. In antecedent conditioned slicing, extra information from the antecedent is used to permit greater pruning of the state space. In a previous version of this paper, we applied antecedent conditioned slicing to safety properties of the form G(antecedent ⇒ consequent) where antecedent and consequent were written in propositional logic. In this paper, we use antecedent conditioned slicing to handle safety and bounded liveness property specifications written in linear time temporal logic. We present a theoretical justification of our technique. We provide experimental results on a Verilog RTL implementation of the USB 2.0 functional core, which is a large design with about 1,100 state elements (10³³¹ states). The results demonstrate that the technique provides significant performance benefits over static program slicing using state-of-the-art model checkers.     

Program model checking as a new trend

This paper introduces a special section of the STTT journal containing a selection of papers that were presented at the 7th international SPIN workshop, Stanford, 30 August – 1 September 2000. The workshop was named SPIN Model Checking and Software Verification, with an emphasis on model checking of programs. The paper outlines the motivation for stressing software verification, rather than only design and model verification, by presenting the work done in the Automated Software Engineering group at NASA Ames Research Center within the last 5 years. This includes work in software model checking, testing like technologies and static analysis. Published online: 2 October 2002     

Comparison of SPIN and VIS for protocol verification

In this paper, we compare and contrast SPIN and VIS, two widely used formal verification tools. In particular, we devote special attention to the efficiency of these tools for the verification of communications protocols that can be implemented either in software or hardware. As a basis of our comparison, we formally describe and verify the Asynchronous Transfer Mode Ring (ATMR) medium access protocol using SPIN and its hardware model using VIS. We believe that this study is of particular interest as more and more protocols, like ATM protocols, are implemented in hardware to match high-speed requirements. Published online: 1 March 2002     

Preface by the section editor

The papers in this special section present a sampling of new symbolic approaches for determining whether or not a system satisfies its specification. Abstracts of these articles appeared originally in the Proceedings of the 1999 Symposium on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’99). Published online: 18 July 2001     

Model checking: a hardware design perspective

Current practices in the verification of commercial hardware designs (digital, synchronous, and sequential semiconductors) are described. Recent advances in verification by the mathematical technique called model checking are described, and requirements for the successful application of model checking in commercial design are discussed.     

Automatically Detecting and Visualising Errors in UML Diagrams

UML has become the de facto standard for object-oriented modelling. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we developed a formalisation framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This paper describes automated structural and behavioural analyses applicable to UML diagrams using our formalisation framework. In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem for behavioural analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modelling and analysis of UML diagrams for an automotive industrial case study. Correspondence and offprint requests to: Dr B. Cheng, Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, 3115 Engineering Building, East Lansing, MI 48824, USA. Tel.: +1 517 355 8344; Fax: +1 517 432 1061; Email: chengb@cse.msu.edu     

Managing the verification trajectory

In this paper we take a closer look at the automated analysis of designs, in particular of verification by model checking. Model checking tools are increasingly being used for the verification of real-life systems in an industrial context. In addition to ongoing research aimed at curbing the complexity of dealing with the inherent state space explosion problem – which allows us to apply these techniques to ever larger systems – attention must now also be paid to the methodology of model checking, to decide how to use these techniques to their best advantage. Model checking “in the large” causes a substantial proliferation of interrelated models and model checking sessions that must be carefully managed in order to control the overall verification process. We show that in order to do this well both notational and tool support are required. We discuss the use of software configuration management techniques and tools to manage and control the verification trajectory. We present Xspin/Project, an extension to Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin. Published online: 18 June 2002     

Higher-level techniques for hardware description and synthesis

The FLaSH (Functional Languages for Synthesising Hardware) system allows a designer to map a high-level functional language, SAFL, and its more expressive extension, SAFL+, into hardware. The system has two phases: first we perform architectural exploration by applying a series of semantics-preserving transformations to SAFL specifications; then the resulting specification is compiled into hardware in a resource-aware manner – that is, we map separate functions to separate hardware functional units (functions which are called multiple times become shared functional units). This article introduces the SAFL language and shows how program transformations on it can explore area-time trade-offs. We then show how the FLaSH compiler compiles SAFL to synchronous hardware and how SAFL transformations can also express hardware/software co-design. As a case study we demonstrate how SAFL transformations allow us to refine a simple specification of a MIPS-style processor into pipelined and superscalar implementations. The superset language SAFL+ (adding process calculi features but retaining many of the design aims) is then described and given semantics both as hardware and as a programming language. Published online: 17 December 2002     

Model checking JAVA programs using JAVA PathFinder

This paper describes a translator called Java PathFinder (Jpf), which translates from Java to Promela, the modeling language of the Spin model checker. Jpf translates a given Java program into a Promela model, which then can be model checked using Spin. The Java program may contain assertions, which are translated into similar assertions in the Promela model. The Spin model checker will then look for deadlocks and violations of any stated assertions. Jpf generates a Promela model with the same state space characteristics as the Java program. Hence, the Java program must have a finite and tractable state space. This work should be seen in a broader attempt to make formal methods applicable within NASA’s areas such as space, aviation, and robotics. The work is a continuation of an effort to formally analyze, using Spin, a multi-threaded operating system for the Deep-Space 1 space craft, and of previous work in applying existing model checkers and theorem provers to real applications.     

非经典切片技术及其在形式验证中的应用综述

切片技术最初是作为一种程序分解抽取的分析技术而出现的,经过20多年的不断发展和完善,应用范围已遍及软件工程学科的各个方面。特别是从本世纪初,随着非经典切片：计算切片和证明切片两个新兴研究方向的出现,其学术研究和工程价值越发突出。简要地介绍了切片技术思想的起源、发展过程,并着重介绍非经典的计算切片和证明切片技术及其在验证领域的应用。     

A systematic incrementalization technique and its application to hardware design

A systematic transformation method based on incrementalization and value caching generalizes a broad family of program optimizations. It yields significant performance improvements in many program classes, including iterative schemes that characterize hardware specifications. CACHET is an interactive incrementalization tool. Although incrementalization is highly structured and automatable, better results are obtained through interaction, where the main task is to guide term rewriting based on data-specific identities. Incrementalization specialized to iteration corresponds to strength reduction, a familiar program improvement technique. This correspondence is illustrated by the derivation of a hardware-efficient nonrestoring square-root algorithm, which has also served as an example of theorem prover-based implementation verification. Published online: 9 October 2001 RID="*" ID="*"S.D. Johnson supported, in part, by the National Science Foundation under grant MIP-9601358. RID="**" ID="**"Y.A. Liu supported in part by the National Science Foundation under grant CCR-9711253, the Office of Naval Research under grant N00014-99-1-0132, and Motorola Inc. under a Motorola University Partnership in Research Grant. RID="***" ID="***"Y. Zhang is a student recipient of a Motorola University Partnership in Research Grant.     

SOCKET通信程序模型抽取及可靠性验证

形式化方法是验证并发系统可靠性和安全性的重要手段。对高级语言开发的并发系统自动抽取的模型进行 形式化验证是模型检测技术领域中的一个研究热点。鉴于socket函数调用顺序不正确产生的运行时潜在问题(内存 泄漏、死锁、边界数据丢失等),针对顺序结构的socket程序,通过描述Promcla消息数据结构和通道,构建socket函数 的Promcla模型,定义socket函数到Promcla映射规则,提出socket函数调用序列抽取算法及目标Promcla模型生成 算法,用线性时态逻辑(LTI.)刻画socket函数调用顺序应满足的性质,开发基于SPIN的socket通信程序分析系统。 实验结果表明,该系统能有效检测socket通信程序的运行时潜在问题。     

Benchmarking finite-state verifiers

A variety of largely automated methods have been proposed for finite-state verification of computer systems. Although anecdotal accounts of success are widely reported, there is very little empirical data on the relative strengths and weaknesses of those methods across a broad range of analysis questions and systems. This information, however, is critical for the transfer of the technology from research to practice. We review some of the problems involved in obtaining this information and suggest several ways in which the community can facilitate empirical evaluation of finite-state verification tools.     

Using symbolic CTL model checking to verify the railway stations of Hoorn-Kersenboogerd and Heerhugowaard

We examine the application of symbolic CTL model checking to railway interlocking software. We show that the railway interlocking systems examined exhibit the characteristics of robustness and locality, and that these characteristics allow optimizations to the model checking algorithms not possible in the general case. In order to gain a better understanding of robustness and locality, we examine in detail a small railway interlocking. Published online: 9 October 2001     

Verification and optimization of a PLC control schedule

We report on the use of model checking techniques for both the verification of a process control program and the derivation of optimal control schedules. Most of this work has been carried out as part of a case study for the EU VHS project (Verification of Hybrid Systems), in which the program for a Programmable Logic Controller (PLC) of an experimental chemical plant had to be designed and verified. The original intention of our approach was to see how much could be achieved here using the standard model checking environment of SPIN/Promela. As the symbolic calculations of real-time model checkers can be quite expensive it is interesting to try and exploit the efficiency of established non-real-time model checkers like SPIN in those cases where promising work-arounds seem to exist. In our case we handled the relevant real-time properties of the PLC controller using a time-abstraction technique; for the scheduling we implemented in Promela a so-called variable time advance procedure . To compare and interpret the results we carried out the same case study with the aid of the real-time model checker Uppaal, enhanced with facilities for cost-guided state space exploration. Both approaches proved sufficiently powerful to verify the design of the controller and/or derive (time-)optimal schedules within reasonable time and space requirements. Published online: 2 October 2002 The work reported here was carried out while the second and third authors were employed by the Computer Science Department of the University of Nijmegen, Netherlands. The second author was supported by an NWO postdoc grant, the third author by an NWO PhD grant, and both were supported by the EU LTR project VHS (Project No. 26270).