A framework for table driven testing of Java classes

With the advent of object-oriented languages and the portability of Java, the development and use of class libraries has become widespread. Effective class reuse depends on class reliability which in turn depends on thorough testing. This paper describes a class testing approach based on modeling each test case with a tuple and then generating large numbers of tuples to thoroughly cover an input space with many interesting combinations of values. The testing approach is supported by the Roast framework for the testing of Java classes. Roast provides automated tuple generation based on boundary values, unit operations that support driver standardization, and test case templates used for code generation. Roast produces thorough, compact test drivers with low development and maintenance cost. The framework and tool support are illustrated on a number of non-trivial classes, including a graphical user interface policy manager. Quantitative results are presented to substantiate the practicality and effectiveness of the approach. Copyright (C) 2002 John Wiley Sons, Ltd.

The variety of variables in automated real-time refinement

The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.

An approach to verifying and debugging simulation models governed by ordinary differential equations: Part 1. Methodology for residual generation

For dynamic simulations to be credible, verification of the computer code must be an integral part of the modelling process. This two-part paper describes a novel approach to verification through program testing and debugging. In Part 1, a methodology is presented for detecting and isolating coding errors using back-to-back testing. Residuals are generated by comparing the output of two independent implementations, in response to identical inputs. The key feature of the methodology is that a specially modified observer is created using one of the implementations, so as to impose an error-dependent structure on these residuals. Each error can be associated with a fixed and known subspace, permitting errors to be isolated to specific equations in the code. It is shown that the geometric properties extend to multiple errors in either one of the two implementations. Copyright (C) 2003 John Wiley Sons, Ltd.

CXTANNEAL: an improved program for estimating solute transport parameters

CXTANNEAL is a program for analysing contaminant transport in soils. The code, written in Fortran 77, is a modified version of CXTFIT, a commonly used package for estimating solute transport parameters in soils. The improvement of the present code is that it includes simulated annealing as the optimization technique for curve fitting. Tests with hypothetical data show that CXTANNEAL performs better than the original code in searching for optimal parameter estimates. To reduce the computational time, a parallel version of CXTANNEAL (CXTANNEAL_P) was also developed. (C) 1999 Elsevier Science Ltd. All rights reserved.

A formal model of real-time program compilation

Program compilation can be formally defined as a sequence of equivalence-preserving transformations, or refinements, from high-level language programs to assembler code, Recent models also incorporate timing properties, but the resulting formalisms are intimidatingly complex. Here we take advantage of a new, simple model of real-time refinement, based on predicate transformer semantics, to present a straightforward compilation formalism that incorporates real-time constraints. (C) 2002 Elsevier Science B.V. All rights reserved.

API documentation with executable examples

The rise of component-based software development has created an urgent need for effective application program interface (API) documentation. Experience has shown that it is hard to create precise and readable documentation. Prose documentation can provide a good overview but lacks precision. Formal methods offer precision but the resulting documentation is expensive to develop. Worse, few developers have the skill or inclination to read formal documentation. We present a pragmatic solution to the problem of API documentation. We augment the prose documentation with executable test cases, including expected outputs, and use the prose plus the test cases as the documentation. With appropriate tool support, the test cases are easy to develop and read. Such test cases constitute a completely formal, albeit partial, specification of input/output behavior. Equally important, consistency between code and documentation is demonstrated by running the test cases. This approach provides an attractive bridge between formal and informal documentation. We also present a tool that supports compact and readable test cases; and generation of test drivers and documentation, and illustrate the approach with detailed case studies. (C) 2002 Elsevier Science Inc. All rights reserved.

The second generation of the International Equine Gene Mapping Workshop half-sibling linkage map

A low-density, male-based linkage map was constructed as one of the objectives of the International Equine Gene Mapping Workshop. Here we report the second generation map based on testing 503 half-sibling offspring from 13 sire families for 344 informative markers using the crimap program. The multipoint linkage analysis localized 310 markers (90%) with 257 markers being linearly ordered. The map included 34 linkage groups representing all 31 autosomes and spanning 2262 cM with an average interval between loci of 10.1 cM. This map is a milestone in that it is the first map with linkage groups assigned to each of the 31 automosomes and a single linkage group to all but three chromosomes.

Procedures and parameters in the real-time program refinement calculus

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints oil when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire. For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler. (c) 2006 Elsevier B.V. All rights reserved.

The next generation messaging technology: Makes web services effective

The vision presented in this paper and its technical content are a result of close collaboration between several researchers from the University of Queensland, Australia and the SAP Corporate Research Center, Brisbane, Australia. In particular; Dr Wasim Sadiq (SAP), Dr Shazia Sadiq (UQ), and Dr Karsten Schultz (SAP) are the prime contributors to the ideas presented. Also, PhD students Mr Dat Ma Cao and Ms Belinda Carter are involved in the research program. Additionally, the Australian Research Council Discovery Project Scheme and Australian Research Council Linkage Project Scheme support some aspects of research work towards the HMT solution.

UML approach to the generation of test sequences for Java-based concurrent systems

Starting with a UML specification that captures the underlying functionality of some given Java-based concurrent system, we describe a systematic way to construct, from this specification, test sequences for validating an implementation of the system. The approach is to first extend the specification to create UML state machines that directly address those aspects of the system we wish to test. To be specific, the extended UML state machines can capture state information about the number of waiting threads or the number of threads blocked on a given object. Using the SAL model checker we can generate from the extended UML state machines sequences that cover all the various possibilities of events and states. These sequences can then be directly transformed into test sequences suitable for input into a testing tool such as ConAn. As an illustration, the methodology is applied to generate sequences for testing a Java implementation of the producer-consumer system. © 2005 IEEE

A technique for modular logic program refinement

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we introduce modules into a logic programming refinement calculus. Modules allow data types to be grouped together with sets of procedures that manipulate the data types. By placing restrictions on the way a program uses a module, we develop a technique for refining the module so that it uses a more efficient representation of the data type.

Effects of temperature-dependent viscosity variation on entropy generation, heat and fluid flow through a porous-saturated duct of rectangular cross-section

Effect of temperature-dependent viscosity on fully developed forced convection in a duct of rectangular cross-section occupied by a fluid-saturated porous medium is investigated analytically. The Darcy flow model is applied and the viscosity-temperature relation is assumed to be an inverse-linear one. The case of uniform heat flux on the walls, i.e. the H boundary condition in the terminology of Kays and Crawford, is treated. For the case of a fluid whose viscosity decreases with temperature, it is found that the effect of the variation is to increase the Nusselt number for heated walls. Having found the velocity and the temperature distribution, the second law of thermodynamics is invoked to find the local and average entropy generation rate. Expressions for the entropy generation rate, the Bejan number, the heat transfer irreversibility, and the fluid flow irreversibility are presented in terms of the Brinkman number, the Péclet number, the viscosity variation number, the dimensionless wall heat flux, and the aspect ratio (width to height ratio). These expressions let a parametric study of the problem based on which it is observed that the entropy generated due to flow in a duct of square cross-section is more than those of rectangular counterparts while increasing the aspect ratio decreases the entropy generation rate similar to what previously reported for the clear flow case.

Heat transfer and entropy generation optimization of forced convection in a porous-saturated duct of rectangular cross-section

We investigate analytically the first and the second law characteristics of fully developed forced convection inside a porous-saturated duct of rectangular cross-section. The Darcy-Brinkman flow model is employed. Three different types of thermal boundary conditions are examined. Expressions for the Nusselt number, the Bejan number, and the dimensionless entropy generation rate are presented in terms of the system parameters. The conclusions of this analytical study will make it possible to compare, evaluate, and optimize alternative rectangular duct design options in terms of heat transfer, pressure drop, and entropy generation. (c) 2006 Elsevier Ltd. All rights reserved.

Diagnostics of A Range of Highly Superorbital Carbon Dioxide Flows

Expansion tubes are impulse facilities capable of generating highly energetic hyper-sonic flows. This work surveys a broad range of flow conditions produced in the facility X1 with carbon dioxide test gas, for simulation of spacecraft entry into the Martian atmosphere. Conditions with nominal flow speeds of 7, 9, 11 and 13 km/s were tested. The freestream conditions were calibrated using static/Pitot pressure measurements and advanced optical diagnostics. An extensive set of holographic interferometry experiments was performed on flows over wedges for quantitative study of freestream and post-shock densities, and post-shock ionisation. A one-dimensional code with frozen and equilibrium chemistry capabilities was used to estimate the freestream conditions. An equilibrium chemistry model produced a good match to measured freestream quantities at the high enthalpy conditions which are a major aim of this facility's operation. The freestream in the lower enthalpy conditions was found to be heavily influenced by chemical non-equilibrium. Non-equilibrium in the final unsteady expansion process of flow generation was accounted for by switching from equilibrium to frozen chemistry at a predetermined point. Comparison between the freestream density results of holographic interferometry, pressure measurements and computations shows good agreement.