Proof engineering in the large: formal verification of Pentium®4 floating-point divider

We examine the challenges presented by large-scale formal verification of industrial-size circuits, based on our experiences in verifying the class of all micro-operations executing on the floating-point division and square root unit of the Intel IA-32 Pentium?4 microprocessor. The verification methodology is based on combining human-guided mechanised theorem-proving with low-level steps verified by fully automated model-checking. A key observation in the work is the need to explicitly address the issues of proof design and proof engineering, i.e., the process of creating proofs and the craft of structuring and formulating them, as concerns on their own right. Published online: 19 November 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     

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     

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     

Mechanized result verification: an industrial application

We present part of an industrial project where mechanized theorem proving is used for the validation of a translator which generates safety critical software. In this project, the mechanized proof is decomposed in two parts: one is done “online”, at each run of the translator, by a custom prover which checks automatically that the result of each translation meets some verification conditions; the other is done “offline”, once for all, interactively with a general purpose prover; the offline proof shows that the verification conditions checked by the online prover are sufficient to guarantee the correctness of each translation. The provably correct verification conditions can thus be seen as specifications for the online prover. This approach is called mechanized result verification. This paper describes the project requirements and explains the motivations to formal validation by mechanized result verification, provides an overview of the formalization of the specifications for the online prover and discusses in detail some issues we have addressed in the mechanized offline proof.     

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.     

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).     

Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k

This paper reports on the mechanical verification of the IEEE 1394 root contention protocol. This is an industrial leader election protocol, in which timing parameters play an essential role. A manual verification of this protocol using I/O automata has been published in [24]. We improve the communication model presented in that paper. Using the Uppaal2k tool, we investigate the timing constraints on the parameters which are necessary and sufficient for correct protocol operation: by analyzing large numbers of protocol instances with different parameter values, we derive the required timing constraints. We explore the use of model checking in combination with stepwise abstraction. That is, we show that the implementation automaton correctly implements the specification via several intermediate automata, using Uppaal to prove the trace inclusion in each step. Published online: 18 July 2001     

Expressing checkable properties of dynamic systems: the Bandera Specification Language

Research on how to reason about correctness properties of software systems using model checking is advancing rapidly. Work on extracting finite-state models from program source code and on abstracting those models is focused on enabling the tractable checking of program properties such as freedom from deadlock and assertion violations. For the most part, the problem of specifying more general program properties has not been considered. In this paper, we report on the support for specifying properties of dynamic multi-threaded Java programs that we have built into the Bandera system. Bandera extracts finite-state models, in the input format of several existing model checkers, from Java code based on the property to be checked. The Bandera Specification Language (BSL) provides a language for defining general assertions and pre/post conditions on methods. It also supports the definition of observations that can be made of the state of program objects and the incorporation of those observations as predicates that can be instantiated in the scope of object quantifiers and used in describing common forms of state/event sequencing properties. We illustrate how BSL can be used to formulate a variety of system correctness properties for several multi-threaded Java applications. Published online: 2 October 2002     

Formalization and validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN

The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification. We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic (LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface deadlock and problems with the server migration protocol. We also describe how property specification patterns helped us in formalizing the high-level requirements that we have elicited.     

On the Right Track: Systematic Implementation of Ergonomics in Railway Network Control

At a time of change for the railway networks of Europe we have been developing tools to assess ergonomics aspects of railway network control. This is within the Railway Ergonomics Control Assessment Package (RECAP). Among the developments have been an audit instrument (REQUEST), tools to assess situation awareness (RESA) and staff loading (RELOAD), and workshops to predict opportunities for human error and organisational failure across rail network operations. This research is discussed with respect to the context of UK railway operations and the need for an expanding tradition of cognitive ergonomics fieldwork. From the findings we draw some conclusions about the roles filled by signallers, electrical controllers and zone controllers within a perspective of distributed cognitive/social networks.     

Estimations of previewed road curvatures and vehicular motion by a vision-based data fusion scheme

In this study, a new framework of vision-based estimation is developed using some data fusion schemes to obtain previewed road curvatures and vehicular motion states based on the scene viewed from an in-vehicle camera. The previewed curvatures are necessary for the guidance of an automatically steering vehicle, and the desired vehicular motion variables, including lateral deviation, heading angle, yaw rate, and sideslip angle, are also required for proper control of the vehicular lateral motion via steering. In this framework, physical relationships of previewed curvatures among consecutive images, motion variables in terms of image features searched at various levels in the image plane, and dynamic correlation among vehicular motion variables are derived as bases of data fusion to enhance the accuracy of estimation. The vision-based measurement errors are analyzed to determine the fusion gains based on the technique of a Kalman filter such that the measurements from the image plane and predictions of physical models can be properly integrated to obtain reliable estimations. Off-line experimental works using real road scenes are performed to verify the whole framework for image sensing.     

Exploring the Suitability of Virtual Environments for Safety Training: Signals, Norms and Ambiguity in a Simulated Emergency Escape

This study aims at exploring the suitability of virtual environments for safety training in large public spaces. A virtual library was constructed which simulated many of the physical and normative characteristics of the ‘real’ university library which was the target of the virtual safety training project. In the virtual library, two different types of signals (fixed red signs vs. moving green arrows) for guiding people to the emergency exits were presented, and their efficacy on escape times was tested in three different conditions, differing with respect to the distance of participants from the escape exits (measured according to the number of corners separating participants from direct visual discovery of the emergency exit). No significant differences between the different kinds of signals were found, whereas surprising discrepancies among the three conditions appeared. The differences in performance in the three conditions were contingent upon the presence in the virtual library of peculiar environmental features embodying social norms – like a red ribbon indicating no transit. Uncertainty about the sense of such normative features in the context of the simulated emergency made some participants prone to peculiar knowledge-based errors consisting of inadequate sense-making of the normative aspects of the ongoing situation. This kind of error shows that the simulation succeeded in capturing one of the crucial characteristics of ‘real’ social context: ambiguity, which mostly depends on the fact that the social norms structuring public spaces and defining their legitimate uses are often ill defined and context dependent. Every valid experience in safety training requires coping with ambiguity in situations.     

Utilization of stereo disparity and optical flow information for the computer analysis of human interactions

We propose a system that simultaneously utilizes the stereo disparity and optical flow information of real-time stereo grayscale multiresolution images for the recognition of objects and gestures in human interactions. For real-time calculation of the disparity and optical flow information of a stereo image, the system first creates pyramid images using a Gaussian filter. The system then determines the disparity and optical flow of a low-density image and extracts attention regions in a high-density image. The three foremost regions are recognized using higher-order local autocorrelation features and linear discriminant analysis. As the recognition method is view based, the system can process the face and hand recognitions simultaneously in real time. The recognition features are independent of parallel translations, so the system can use unstable extractions from stereo depth information. We demonstrate that the system can discriminate the users, monitor the basic movements of the user, smoothly learn an object presented by users, and can communicate with users by hand signs learned in advance. Received: 31 January 2000 / Accepted: 1 May 2001 Correspondence to: I. Yoda (e-mail: yoda@ieee.org, Tel.: +81-298-615941, Fax: +81-298-613313)     

Networks of Science and Technology in India: The Elite and the Subaltern Streams

The paper investigates the structure and functioning of the science and technology (S&T) system in India as it has evolved in the post-independence period (1947 onwards). The networks of entities involved in S&T actions, the paper argues, can be categorised, in terms of adopted approaches to agenda and priority setting and accounting for actions, into two streams. The origins and expansion of the two streams are traced. One, the ‘Elite’ stream (high profile and visibility linked to big industry), adopting what the paper has generically termed the ‘Nehruvian’ model of development, is shown to have emerged as a dominant network. The other socially powerful ‘Subaltern’ stream (less visible, closer to ground realities and linked to village and cottage industry), adopting the ‘Gandhian’ model of development, still remains dispersed and outside the consideration of high-level decision-making bodies. The paper stresses the importance of moving the support and attention from the dominant stream to efforts that attempt a synthesis between the dominant and the subaltern.