Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Multi-threading and message communication in Qu-Prolog

This paper presents the multi-threading and internet message communication capabilities of Qu-Prolog. Message addresses are symbolic and the communications package provides high-level support that completely hides details of IP addresses and port numbers as well as the underlying TCP/IP transport layer. The combination of the multi-threads and the high level inter-thread message communications provide simple, powerful support for implementing internet distributed intelligent applications.

Using clusters of computers for large QU-GENE simulation experiments

The QU-GENE Computing Cluster (QCC) is a hardware and software solution to the automation and speedup of large QU-GENE (QUantitative GENEtics) simulation experiments that are designed to examine the properties of genetic models, particularly those that involve factorial combinations of treatment levels. QCC automates the management of the distribution of components of the simulation experiments among the networked single-processor computers to achieve the speedup.

An occupational view of the Australian labour force - Patterns of job growth and decline

Generally employment has been studied in terms of changes in the types of goods and services that the economy is purchasing. Far less attention has been given to the occupational aggregates that go into producing these goods and services. The few studies that did investigate this area found that the mix of tabour inputs appear to have been changing over time in a systematic pattern. The increasing prevalence of white-collar, information workers gave rise to the assertion that many societies had entered a post-industrial information age. Deals first of aff with some issues of measurement in the context of the Australian labour force, then looks at trends in various occupational groups using a non-standard four-sector classification of the labour force. Finally suggests an application in relation to the link between education and training and its ability to reduce structural unemployment.

Investigating technical and scale efficiencies of Australian universities through data envelopment analysis

Performance indicators in the public sector have often been criticised for being inadequate and not conducive to analysing efficiency. The main objective of this study is to use data envelopment analysis (DEA) to examine the relative efficiency of Australian universities. Three performance models are developed, namely, overall performance, performance on delivery of educational services, and performance on fee-paying enrolments. The findings based on 1995 data show that the university sector was performing well on technical and scale efficiency but there was room for improving performance on fee-paying enrolments. There were also small slacks in input utilisation. More universities were operating at decreasing returns to scale, indicating a potential to downsize. DEA helps in identifying the reference sets for inefficient institutions and objectively determines productivity improvements. As such, it can be a valuable benchmarking tool for educational administrators and assist in more efficient allocation of scarce resources. In the absence of market mechanisms to price educational outputs, which renders traditional production or cost functions inappropriate, universities are particularly obliged to seek alternative efficiency analysis methods such as DEA.

Materialized view selection under the maintenance time constraint

A data warehouse is a data repository which collects and maintains a large amount of data from multiple distributed, autonomous and possibly heterogeneous data sources. Often the data is stored in the form of materialized views in order to provide fast access to the integrated data. One of the most important decisions in designing a data warehouse is the selection of views for materialization. The objective is to select an appropriate set of views that minimizes the total query response time with the constraint that the total maintenance time for these materialized views is within a given bound. This view selection problem is totally different from the view selection problem under the disk space constraint. In this paper the view selection problem under the maintenance time constraint is investigated. Two efficient, heuristic algorithms for the problem are proposed. The key to devising the proposed algorithms is to define good heuristic functions and to reduce the problem to some well-solved optimization problems. As a result, an approximate solution of the known optimization problem will give a feasible solution of the original problem. (C) 2001 Elsevier Science B.V. All rights reserved.

Developing a meta model for the Bunge-Wand-Weber ontological constructs

At the core of the analysis task in the development process is information systems requirements modelling, Modelling of requirements has been occurring for many years and the techniques used have progressed from flowcharting through data flow diagrams and entity-relationship diagrams to object-oriented schemas today. Unfortunately, researchers have been able to give little theoretical guidance only to practitioners on which techniques to use and when. In an attempt to address this situation, Wand and Weber have developed a series of models based on the ontological theory of Mario Bunge-the Bunge-Wand-Weber (BWW) models. Two particular criticisms of the models have persisted however-the understandability of the constructs in the BWW models and the difficulty in applying the models to a modelling technique. This paper addresses these issues by presenting a meta model of the BWW constructs using a meta language that is familiar to many IS professionals, more specific than plain English text, but easier to understand than the set-theoretic language of the original BWW models. Such a meta model also facilitates the application of the BWW theory to other modelling techniques that have similar meta models defined. Moreover, this approach supports the identification of patterns of constructs that might be common across meta models for modelling techniques. Such findings are useful in extending and refining the BWW theory. (C) 2002 Elsevier Science Ltd. All rights reserved.

Trade and environment: Evidence from China's manufacturing sector

This paper focusing on the Chinese manufacturing sector assesses the environmental impact of trade liberalization in China. The results show that China's experience with the trade liberalization-environment nexus is consistent with international evidence. On one hand, trade liberalization has had various positive effects on the environment. Firstly, it promoted specialization in areas of comparative advantage, which, in general, included industries that contributed less to environmental degradation. Secondly, it allowed China to access and adopt the best international practices in pollution abatement technology. Thirdly, it enabled China to transfer environmental costs to other countries by importing intermediate products whose production contributed to environmental degradation. On the other hand, these positive effects were overwhelmed by a negative scale effect, which was the result of a huge increase in the demand for Chinese exports. The paper concludes that if China is to prevent pollution from reaching a critical threshold, environmental regulations need to be tightened. Copyright (C) 2002 John Wiley & Sons, Ltd and ERP Environment.

The Role of Non-Market Valuation in Forest Management and Recreation Policy

Forests, and particularly those where native and mixed species are gown, provide a variety of non-wood values, important among which are recreation and environmental services. Substantial progress has been made in recent years in estimating economic values on these services. A considerable amount of research on forest values has been carried out recently in tropical and sub-tropical eastern Australia, some of which is reported in the following papers. The need for estimates of non-wood forest benefits is apparent, and it is clear that further development of techniques and a greater understanding of the way these values can be integrated into public-sector decision making is required.

A model of factors affecting an information system's change in state

Management are keen to maximize the life span of an information system because of the high cost, organizational disruption, and risk of failure associated with the re-development or replacement of an information system. This research investigates the effects that various factors have on an information system's life span by understanding how the factors affect an information system's stability. The research builds on a previously developed two-stage model of information system change whereby an information system is either in a stable state of evolution in which the information system's functionality is evolving, or in a state of revolution, in which the information system is being replaced because it is not providing the functionality expected by its users. A case study surveyed a number of systems within one organization. The aim was to test whether a relationship existed between the base value of the volatility index (a measure of the stability of an information system) and certain system characteristics. Data relating to some 3000 user change requests covering 40 systems over a 10-year period were obtained. The following factors were hypothesized to have significant associations with the base value of the volatility index: language level (generation of language of construction), system size, system age, and the timing of changes applied to a system. Significant associations were found in the hypothesized directions except that the timing of user changes was not associated with any change in the value of the volatility index. Copyright (C) 2002 John Wiley Sons, Ltd.