A recent method combines model checkers with specification-based mutation analysis to generate test cases from formal software specifications. However high-level software specifications usually must be reduced to make analysis with a model checker feasible. We propose a new reduction, parts of which can be applied mechanically, to soundly reduce some large, even infinite, state machines to manageable pieces. Our work differs from other work in that we use the reduction for generating test sets as opposed to the typical goal of analyzing for properties. Consequently, we have different criteria, and we prove a different soundness rule. Informally the rule is that counterexamples from the model checker are test cases for the original specification. The reduction changes the state machine and temporal logic constraints in the model checking specification to avoid generating unsound test cases. We give an example of the reduction and test generation.
Software developers use a variety of methods, including both formal methods and testing, to argue that their systems are suitable components for high assurance applications. In this paper, we develop another connection between formal methods and testing by defining a specification-based coverage metric to evaluate test sets. Formal methods in the form of a model checker supply the necessary automation to make the metric practical. The metric gives the software developer assurance that a given test set is sufficiently sensitive to the structure of an application's specification. In this paper, we develop the necessary foundation for the metric and then illustrate the metric on an example.
In a previously developed phase-field model of solidification that includes convection in the melt, the two phases are represented as viscous liquids, where the putative solid phase has a viscosity much larger than the liquid phase. In this paper we report numerical computations on a simplified form of this model which represents the growth of a two-dimensional dendrite in a thin gap between two parallel thermally insulting plates. In these computations flow in the liquid arises because of the differing densities of the solid and liquid phases.
Remote sensing instruments have the ability to collect data over extensive temporal periods and spatial regions. A common thread between all these sensors is the need to relate the measured quantity to a meaningful observation of a system property. If the relationship between each measurement and the set of atmospheric quantities that influence that measurement is known, the problem can be reduced to a set of linear equations. Solving for the unknown atmospheric quantities then becomes a linear algebra problem where the solution vector is equal to the inverse of the kernel matrix multiplied by the set of independent measurements. However, in most remote sensing applications inversion of the kernel matrix is unstable resulting in the amplification of measurement and computational uncertainties. Techniques to circumvent this error amplification have focused on methods of constraining the solution. In this paper we adapt an existing technique to do such an inversion. Noise reduction is accomplished by the addition of double-sided inequality constraints for each unknown variable. The advantage of such a technique is the ability to individually adjust the solution space of each individual unknown depending on a priori knowledge.
The inversion algorithm is applied to the problem of retrieving radar Doppler spectra, which have been artificially broadened by turbulent air motions. First, to test the algorithm, radar Doppler spectra were simulated using known drop-size and vertical air motion distributions. The simulated spectra were used as input to the retrieval algorithm and the results compared to the initial quiet-air spectrum. Results indicate that accurate retrievals can be performed despite the addition of moderate amounts of noise to the simulated spectra. Then, to demonstrate the practical retrieval of quiet-air Doppler spectra, the algorithm was used to process radar observations collected from continental stratocumulus. From these retrievals, a 2-D map of the large-scale vertical motions within the cloud was constructed as well as a profile of vertical velocity variance. In addition, a drop-size distribution was also derived from an updraft region of the cloud.
This paper describes the testing methodology used in ANSI C efficiency testing of the Round 2 Candidates for the Advanced Encryption Standard, along with a few observations regarding those measurements. This paper also has tables of timing and cycle counting values obtained from testing the algorithms. Finally, there are some conclusions regarding which algorithms have the best (i.e., most consistent) performance.
This is a survey of the Metropolis Algorithm for the IEEE special issue on the ten most important algorithms of the century.
This is a tutorial article for the "Computing Prescriptions" column. It explains how to use modular arithmetic in a large computation and why it would be useful.
An implementation is typically checked against a specification by proving that the implementation implies the specification. This ensures that the implementation only has behaviors allowed by the specification. However, this does not require the implementation to have any behavior to all! We propose that correctness statements have two parts, corresponding to liveness and safety. Safety is that the implementation implies an "allowed behavior" specification, as now. Liveness is that a "required behavior" specification implies the implementation.
This paper provides some reflections on the field of mathematical software on the occasion of John Rice's 65th birthday. We describe some of the common themes of research in this field and recall some significant events in its evolution. Finally, we raise a number of issues that are of concern to future developments.
We describe a free energy model that allows the computation of phase diagrams for a particular set of solid-state phase transitions in a binary alloy. This is an extension of our previous work, in which we developed a diffuse-interface model of phase boundaries that occur in order-disorder transitions of a face-centered-cubic (FCC) binary alloy. That model was based on a fourth-order Landau expansion of the free energy function in terms of the three nonconserved order parameters that describe ordering on the underlying FCC lattice. In this paper we examine an improved description of the free energy of the system that incorporates a more realistic dependence on the temperature and composition of the system. The improved model allows the computation of phase diagrams that delineate the states of equilibrium between the various phases that are described by the model. In particular, the phase transition between the disordered FCC phase and the ordered L10 phase is correctly described as a first order phase transition using the improved model, whereas in the previous model this transition was instead modeled as second order. The improved model also allows the self-consistent calculation of concentration variations through interphase boundaries that separate bulk phases, and through antiphase boundaries that separate variants of ordered phases.
We compare the repeated adiabatic shear band formation that takes place at sufficiently large cutting speeds in a number of materials during high-speed machining operations with the more well-known formation of a single shear band that often takes place at sufficiently large strain rates in dynamic torsion tests on these materials. We show that there are several major differences in the physics of the two deformation processes. In particular, the shear stress in machining over the tool-material contact length is not even approximately homogeneous. Additionally, in high-speed machining, the material flow can become convection-dominated, so that the tool can "outrun" the thermal front generated in the workpiece material by the high-strain-rate cutting process. We demonstrate by means of a simple one-dimensional continuum model that these differences can lead to repeated oscillations in the plastic flow of the workpiece material during high-speed machining, leading to the repeated formation of adiabatic shear bands.
Blind deconvolution seeks to deblur an image without knowing the cause of the blur. Iterative methods are commonly applied to that problem, but the iterative process is slow, uncertain, and often ill-behaved. This paper considers a significant but limited class of blurs that can be expressed as convolutions of 2-D symmetric Lévy 'stable' probability density functions. This class includes and generalizes Gaussian and Lorentzian distributions. For such blurs, a method is developed that can detect the point spread function from 1-D Fourier analysis of the blurred image. A separate image deblurring technique uses this detected point spread function to deblur the image. Each of these two steps uses direct non-iterative methods, and requires interactive adjustment of parameters. Using this method, blind deblurring of 512 x 512 images can be accomplished in minutes of CPU time on current desktop workstations. Numerous blind experiments on synthetic data show that for a given blurred image, several distinct point spread functions may be detected that lead to useful yet visually distinct reconstructions.
The National Institute of Standards and Technology (NIST) sponsored the Requirements Group for Real-time Extensions to the Java(tm) Platform. The Requirements Group includes representatives from companies and organizations whose expertise spans the computing industry and academia. Industry participants include desktop, server, and enterprise systems providers, embedded systems providers, device manufacturers, and real-time operating system vendors. The Requirements Group met during a six-month period in a series of open workshops. Additionally, the Requirements Group continued discussions on the rt-java@raleigh.ibm.com mailing list. The goal of the Group was to develop cross-disciplinary requirements for real-time functionality that is expected to be needed by real-time applications written in the Java(tm) programming language and executing on various platforms. This document is the result of the Requirements Group's efforts.
Defining an Access Control Service for an enterprise application requires the choice of an access control model and a process for formulation of access decision rules to be used by the access enforcement mechanism. In this paper, we describe a business process driven framework (called the BPD-ACS) for developing both the model and formulating the access decision rules. The model used is the Role Based Access Control (RBAC) model and the access decision rules are based on temporal business associations. The enterprise setting is a multi-facility hospital and the particular application for which the access control service was defined is the Hospital-based Laboratory Information System. (HLIS).The lesson learnt from this exercise is that a much more sophisticated rule processing capability is required for these types of applications than is currently available in both commercial and research-prototype authorization servers.
The use of XML and its associated APIs, for information modeling and information interchange applications is being actively explored by the research community. In this paper, we develop a XML Document Type Definition (DTD) for representing the schema of a RBAC Model and a conforming XML document containing the actual RBAC-based access control data for a commercial banking application. Based on this DTD, the XML document and the methods in the DOM API Level 1.0 standards, we describe three application tasks related to enterprise-wide implementation of RBAC. They are (a) Implementing a RBAC model for a database application, (b) Implementing RBAC models with identical data on two different database servers, and (c) Transforming data under a RBAC model to a different but structurally similar model like Group-based Access Control model. Other potential Access Control Service applications exploiting the capabilities of some commercial XML processors are also outlined.
The Web has emerged as a dominant mode of making information available and is increasingly seen as the medium to support collaboration across boundaries of geography and time. To realize this potential the Web must support viewing and manipulating of multi-source, multimedia objects that are interdependent, yet must be synchronized temporally and spatially. This paper presents a prototype tool, ACTS, which utilizes the W3C standard Web content technology, Synchronized Multimedia Integrated Language (SMIL), to provide a framework of temporal and spatial synchronization. ACTS is a National Institute of Standards and Technology, Information Technology Laboratory (NIST/ITL) prototype which is based on our S2M2 Java applet-based SMIL player that implements and extends the SMIL 1.0 specification. The ACTS prototype provides
evidence that the Web can become an effective medium for collaboration over multimedia objects.
This paper describes the basic requirements for building an advanced multimedia indexing and retrieval system for annotation collaboration application by using MPEG-7 description schemes (DS) and descriptors (D). These requirements are based on the prototype called ACTS (Annotation Collaboration Tool via SMIL) that was built at the National Institute of Standards and Technology, Information Technology Laboratory (NIST/ITL) for allowing researchers to annotate multimedia objects over the Web. One of the major criteria for this application is the spatial and temporal synchronization between all multimedia objects. This paper utilizes MPEG-7 DSs and Ds from documents such as M5380 [1] and supportive documents as the N2967 [2] and N2997 [3].
In this paper, we propose a bandwidth guaranteed multi-access protocol for broadcast-and-select WDM local networks with a star topology. The proposed protocol is based on a combination of contention and reservation mechanisms for time slotted WDM networks. Every node accesses the data channel by transmitting request packets in minislots on a separate control channel. There are two types of minislots: reservation minislots and contention minislots. Nodes requiring bandwidth guarantees, called guaranteed nodes, use reservation minislots that are assigned by the control node. The remaining nodes share contention minislots using a random access mechanism. Each node dynamically assigns data channels for the minislots successfully returned on a First-Come-First-Served (FCFS) basis. Here, the number of reservation minislots is allocated by the control node. The remaining minislots are used for contention minislots. The reservation minislots can guarantee a minimum bandwidth for the guaranteed nodes. The contention minislots enable on-demand services at the optical layer and achieve good fairness for the remaining bandwidth. This protocol can be implemented with a simple distributed algorithm that efficiently utilizes the data channel.
In the first stage of each run of a neutron lifetime experiment, a magnetic trap is filled with neutrons. In the second stage of each run, decay events plus background events are observed. In a separate experiment, background is measured. The mean lifetime is estimated by fitting a two parameter exponential model to the background corrected data. For two models of the background signal, I determine the optimal ratio of the number of "background only" measurements to the number of primary "neutron decay plus background" measurements. Further, for each run, I determine the optimal allocation of time for filling and for observing decay events. For the case where the background consists of activated aluminum plus a stationary Poisson process, the asymptotic standard error of the lifetime estimate computed from the background corrected data is lower than the asymptotic standard error computed from the uncorrected data. For the case where the background is a stationary Poisson process, background correction is desirable provided that the background intensity is sufficiently small compared to the rate at which neutrons enter the trap.
At NIST, an in-beam neutron lifetime experiment is underway. In part of the experiment, a neutron detector is calibrated. The accuracy of the detector calibration depends, in part, on how accurately the mean wavelength of a neutron beam can be estimated from rocking curve data. Here, rocking curve data is modeled using a Monte Carlo method. To speed up the simulation, an importance sampling method is used. Simulated and observed rocking curves are compared. For simulated data, the statistical bias of the mean wavelength estimate is found to be 0.004 percent.
We present an analysis of the current tradeoffs between using copper wire versus fiberoptic cable for rewiring buildings at NIST for data communications to the desk-top. We consider tradeoffs from two different viewpoints: (a) the cost of installing and maintaining the wiring, and (b) the computer imposed limitations on the use of the wiring. These findings substantiate our decision to use copper wiring.
Delta-CRLs were designed to provide a more efficient way to distribute certificate status information. However, as this paper will show, in some environments, if delta-CRLs are used as was originally intended, the benefits of using delta-CRLs will be minimal. This paper provides an analysis of delta-CRLs demonstrating the problems associated with issuing delta-CRLs in the "traditional" manner. A more efficient technique for issuing delta-CRLs is then presented.
The effect of the instantaneous application of an electric current during the directional solidification of a binary alloy is considered. The initial state consists of steady-state solidification at constant velocity. It is assumed that the electric current is sufficiently small that its application can be treated as a small perturbation. The problem is solved by Laplace transform techniques and the results are compared to numerical calculations for arbitrary currents. The Laplace transform allows for an understanding of the discontinuities resulting from the discontinuous electric pulse.
The performance drive of parallel computing and platform upgrades or replacements are among the reasons frequent running of benchmark codes has become commonplace for application and platform evaluation and tuning. NIST is developing a prototype for an automated benchmarking toolset to reduce the manual effort in running and analyzing the results of such benchmarks. Our toolset consists of three main modules. A Data Collection and Storage module handles the collection of performance data and implements a central repository for such data. Another module provides an integrated mechanism to analyze and visualize the data stored in the repository. An Experiment Control Module assists the user in designing and executing experiments. To reduce the development effort this toolset is built around existing tools and is designed to be easily extensible to support other tools.
A number of projects within the National Institute of Standards and Technology (NIST) have addressed the visual presentation and evaluation of search results. Within the design space for this problem, we distinguish between the logical structure imposed on the result set and the interface by which the structured results are presented to the user. This interface comprises the operations provided for the manipulation of the set as well as its visual presentation. Any design, no matter how intuitively appealing, should be evaluated and the full array of issues for HCI testing come into play. In particular, researchers must decide on a base case against which to measure, whether to use high-level and/or low-level metrics and which tasks are appropriate for the evaluation.
Experimental results on solute microsegregation induced by Peltier Interface Demarcation (PID) technique during directional solidification of Bi - 1 wt % Sb alloys are presented. Using these data and numerical simulation, the theory of PID is revisited. It is shown that the limited growth kinetics has a dominant effect so that the commonly made assumption of local equilibrium at the solid-liquid interface (i.e., usual hypothesis of constant interface temperature during pulse marking for pure systems) should be abandoned, and the right dependence of interface temperature on solidification velocity included in the model. Consequently, the Peltier coefficients previously determined using Peltier pulsing have been more or less underestimated. Finally, two conditions to select systems capable of efficient marking by PID microsegregation are deduced and the effects of applied current in the first instants of electric pulse clarified.
The 4-D/Real-Time Control System (RCS) Reference Model Architecture provides a well-defined strategy for development of software components for applications in robotics, automated manufacturing, and autonomous vehicles. An investigation has been conducted into the use of Architectural Description Languages (ADLs) as a means to provide a more formal, rigorous definition of the 4-D/RCS architecture and to specify software components for 4-D/RCS systems. In this report, we describe the results of an experiment into the use of an ADL to specify 4-D/RCS systems and assess the potential value of ADLs as specification and development tools for RCS domain experts. We conclude that ADLs not only can be used successfully to specify the 4-D/RCS Reference Model, but that they also serve as effective tools to enhance and extend this model. We also find that ADLs potentially can provide a formal basis for automatically checking the consistency of architecture specifications and verifying that designs conform to the reference architecture.This report discusses prospects for automated reuse of components specified with an ADL and makes recommendations on improving ADLs as effective tools for specifying, communicating, and validating 4-D/RCS system designs and software components. Finally the report discusses potential influence of ADLs for commercial software development tools and provides future directions for research.
Today's state of the art information retrieval document ranking functions contain several tuning parameters. The proper settings for these parameters for a given collection may not be known and may be difficult to derive. This paper reports on efforts to derive a document ranking function with a single tuning parameter that can be set once and will work across many different collections. The performance target for this function is to meet or exceed the performance level of the top weighting functions as evaluated in the TREC conference. To achieve this goal experiments were carried out on several simple weighting functions using pivoted document length normalization to improve their performance. The results show that good performance can be achieved by using a simple pivoted normalization function that works well across the collections used in this study.
NIST solicited candidate algorithms for the Advanced Encryption Standard in a Federal Register Announcement dated September 12, 1997. Fifteen candidates were submitted, and NIST has subsequently worked with a worldwide community of cryptanalysts and computer security researchers to analyze these candidates. This paper documents the test environment created by NIST for this purpose and the test results. Candidates were tested for memory usage, speed, and complexity. A final ranking of the candidates was obtained by normalizing the raw test results and calculating final composite scores that reflect performance across all test categories.