A framework and tool support for the systematic testing of model-based specifications

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.

Dealing with non-determinism in testing concurrent java components

The testing of concurrent software components can be difficult due to the inherent non-determinism present in these components. For example, if the same test case is run multiple times, it may produce different results. This non-determinism may lead to problems with determining expected outputs. In this paper, we present and discuss several possible solutions to this problem in the context of testing concurrent Java components using the ConAn testing tool. We then present a recent extension to the tool that provides a general solution to this problem that is sufficient to deal with the level of non-determinism that we have encountered in testing over 20 components with ConAn. © 2005 IEEE

On building a principled framework for evaluating and testing evolutionary algorithms: A continuous landscape generator

In this paper, we address some issue related to evaluating and testing evolutionary algorithms. A landscape generator based on Gaussian functions is proposed for generating a variety of continuous landscapes as fitness functions. Through some initial experiments, we illustrate the usefulness of this landscape generator in testing evolutionary algorithms.

Concepts and tools for comprehensive sustainability assessments for tourism destinations: a comparative review

This paper reviews a wide range of tools for comprehensive sustainability assessments at whole tourism destinations, covering socio-cultural, economic and environmental issues. It considers their strengths, weaknesses and site specific applicability. It is intended to facilitate their selection (and combination where necessary). Tools covered include Sustainability Indicators, Environmental Impact Assessment, Life Cycle Assessment, Environmental Audits, Ecological Footprints, Multi-Criteria Analysis and Adaptive Environmental Assessment. Guidelines for evaluating their suitability for specific sites and situations are given as well as examples of their use.

Linearly-increasing-stress testing of carbon steel in 4 N NaNO3 and in Bayer liquor

This paper reports the application of linearly increasing stress testing (LIST) to the study of stress corrosion cracking (SCC) of carbon steel in 4 N NaNO3 and in Bayer liquor. LIST is similar to the constant extension-rate testing (CERT) methodology with the essential difference that the LIST is load controlled whereas the CERT is displacement controlled. The main conclusion is that LIST is suitable for the study of the SCC of carbon steels in 4 N NaNO3 and in Bayer liquor. The low crack velocity in Bayer liquor and a measured maximum stress close to that of the reference specimen in air both indicate that a low applied stress rate is required to study SCC in this system. (C) 1998 Chapman & Hall.

Improving wheat simulation capabilities in Australia from a cropping systems perspective - II. Testing simulation capabilities of wheat growth

To simulate cropping systems, crop models must not only give reliable predictions of yield across a wide range of environmental conditions, they must also quantify water and nutrient use well, so that the status of the soil at maturity is a good representation of the starting conditions for the next cropping sequence. To assess the suitability for this task a range of crop models, currently used in Australia, were tested. The models differed in their design objectives, complexity and structure and were (i) tested on diverse, independent data sets from a wide range of environments and (ii) model components were further evaluated with one detailed data set from a semi-arid environment. All models were coded into the cropping systems shell APSIM, which provides a common soil water and nitrogen balance. Crop development was input, thus differences between simulations were caused entirely by difference in simulating crop growth. Under nitrogen non-limiting conditions between 73 and 85% of the observed kernel yield variation across environments was explained by the models. This ranged from 51 to 77% under varying nitrogen supply. Water and nitrogen effects on leaf area index were predicted poorly by all models resulting in erroneous predictions of dry matter accumulation and water use. When measured light interception was used as input, most models improved in their prediction of dry matter and yield. This test highlighted a range of compensating errors in all modelling approaches. Time course and final amount of water extraction was simulated well by two models, while others left up to 25% of potentially available soil water in the profile. Kernel nitrogen percentage was predicted poorly by all models due to its sensitivity to small dry matter changes. Yield and dry matter could be estimated adequately for a range of environmental conditions using the general concepts of radiation use efficiency and transpiration efficiency. However, leaf area and kernel nitrogen dynamics need to be improved to achieve better estimates of water and nitrogen use if such models are to be use to evaluate cropping systems. (C) 1998 Elsevier Science B.V.

The Swiss heroin trials: testing alternative approaches

Over half a million heroin misusers receive oral methadone maintenance treatment world-wide1 but the maintenance prescription of injectable opioid drugs, like heroin, remains controversial. In 1992 Switzerland began a large scale evaluation of heroin and other injectable opiate prescribing that eventually involved 1035 misusers. 2 3 The results of the evaluation have recently been reported.4 These show that it was feasible to provide heroin by intravenous injection at a clinic, up to three times a day, for seven days a week. This was done while maintaining good drug control, good order, client safety, and staff morale. Patients were stabilised on 500 to 600 mg heroin daily without evidence of increasing tolerance. Retention in treatment was 89% at six months and 69% at 18 months.4 The self reported use of non-prescribed heroin fell signifianctly, but other drug use was minimally affected. The death rate was 1% per year, and there were no deaths from overdose among participants . . . [Full text of this article]

Formal derivation of finite state machines for class testing

Previous work on generating state machines for the purpose of class testing has not been formally based. There has also been work on deriving state machines from formal specifications for testing non-object-oriented software. We build on this work by presenting a method for deriving a state machine for testing purposes from a formal specification of the class under test. We also show how the resulting state machine can be used as the basis for a test suite developed and executed using an existing framework for class testing. To derive the state machine, we identify the states and possible interactions of the operations of the class under test. The Test Template Framework is used to formally derive the states from the Object-Z specification of the class under test. The transitions of the finite state machine are calculated from the derived states and the class's operations. The formally derived finite state machine is transformed to a ClassBench testgraph, which is used as input to the ClassBench framework to test a C++ implementation of the class. The method is illustrated using a simple bounded queue example.

Weathering of hydrocarbons in mangrove sediments: testing the effects of using dispersants to treat oil spills

This field study was a combined chemical and biological investigation of the relative effects of using dispersants to treat oil spills impacting mangrove habitats. The aim of the chemistry was to determine whether dispersant affected the short- or long-term composition of a medium range crude oil (Gippsland) stranded in a tropical mangrove environment in Queensland, Australia. Sediment cores from three replicate plots of each treatment (oil only and oil plus dispersant) were analyzed for total hydrocarbons and for individual molecular markers (alkanes, aromatics, triterpanes, and steranes). Sediments were collected at 2 days, then 1, 7, 13 and 22 months post-spill. Over this time, oil in the six treated plots decreased exponentially from 36.6 +/- 16.5 to 1.2 +/- 0.8 mg/g dry wt. There was no statistical difference in initial oil concentrations, penetration of oil to depth, or in the rates of oil dissipation between oiled or dispersed oil plots. At 13 months, alkanes were >50% degraded, aromatics were similar to 30% degraded based upon ratios of labile to resistant markers. However, there was no change in the triterpane or sterane biomarker signatures of the retained oil. This is of general forensic interest for pollution events. The predominant removal processes were evaporation (less than or equal to 27%) and dissolution (greater than or equal to 56%), with a lag-phase of 1 month before the start of significant microbial degradation (less than or equal to 7%). The most resistant fraction of the oil that remained after 7 months (the higher molecular weight hydrocarbons) correlated with the initial total organic carbon content of the soil. Removal rate in the Queensland mangroves was significantly faster than that observed in the Caribbean and was related to tidal flushing. (C) 1999 Elsevier Science Ltd. All rights reserved.

A model of specification-based testing of interactive systems

In this paper we present a model of specification-based testing of interactive systems. This model provides the basis for a framework to guide such testing. Interactive systems are traditionally decomposed into a functionality component and a user interface component; this distinction is termed dialogue separation and is the underlying basis for conceptual and architectural models of such systems. Correctness involves both proper behaviour of the user interface and proper computation by the underlying functionality. Specification-based testing is one method used to increase confidence in correctness, but it has had limited application to interactive system development to date.