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.

Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.

Peace beyond the State? NGOs in Bosnia and Herzegovina

By examining the work of several NGOs in the context of post-conflict reconstruction in Bosnia and Herzegovina (BiH), this essay scrutinizes both the potential and limits of NGO contributions to peace-settlements and long-term stability. While their ability to specialize and reach the grassroots level is of great practical significance, the contribution of NGOs to the reconstruction of war-torn societies is often idealized. NGOs remain severely limited by ad hoc and project-specific funding sources, as well as by the overall policy environment in which they operate. Unless these underlying issues are addressed, NGOs will ultimately become little more than extensions of prevalent multilateral and state-based approaches to post-conflict reconstruction.

Formal verification of ASM designs using the MDG tool

In this paper, we present a formal hardware verification framework linking ASM with MDG. ASM (Abstract State Machine) is a state based language for describing transition systems. MDG (Multiway Decision Graphs) provides symbolic representation of transition systems with support of abstract sorts and functions. We implemented a transformation tool that automatically generates MDG models from ASM specifications, then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models. We support this work with a case study of an Island Tunnel Controller, which behavior and structure were specified in ASM then using our ASM-MDG tool successfully verified within the MDG tool.

Quantum dynamics as a physical resource

How useful is a quantum dynamical operation for quantum information processing? Motivated by this question, we investigate several strength measures quantifying the resources intrinsic to a quantum operation. We develop a general theory of such strength measures, based on axiomatic considerations independent of state-based resources. The power of this theory is demonstrated with applications to quantum communication complexity, quantum computational complexity, and entanglement generation by unitary operations.

Cadence, war and security

An increased incidence of attack has been identified as a major characteristic of the new threat posed by terrorist groups such as al Qaeda. This article considers what such a change means for Western national security systems by examining bow different parts of the system change over time. It becomes evident that Western national security systems are structured on an assumption of comparatively slow state-based threats. In contrast, terrorist franchises operate at a faster pace, are more 'lightweight' and can adapt within the operational and capability cycles of Western governments. Neither network-centric warfare nor an improved assessment of the threat, called for by some, offers a panacea in this regard. Rather, it is clear that not only do Western governments need to adjust their operational and capability cycles, but that they also need a greater diversity of responses to increase overall national security resilience and offer more tools for policy-makers.

Optimal unravellings for feedback control in linear quantum systems

For quantum systems with linear dynamics in phase space much of classical feedback control theory applies. However, there are some questions that are sensible only for the quantum case: Given a fixed interaction between the system and the environment what is the optimal measurement on the environment for a particular control problem? We show that for a broad class of optimal (state- based) control problems ( the stationary linear-quadratic-Gaussian class), this question is a semidefinite program. Moreover, the answer also applies to Markovian (current-based) feedback.

Searching for cancer deaths in Australia: National Death Index vs Cancer Registries

OBJECTIVE: To compare the accuracy, costs and utility of using the National Death Index (NDI) and state-based cancer registries in determining the mortality status of a cohort of women diagnosed with ovarian cancer in the early 1990s. METHODS: As part of a large prognostic study, identifying information on 822 women diagnosed with ovarian cancer between 1990 and 1993, was simultaneously submitted to the NDI and three state-based cancer registries to identify deceased women as of June 30, 1999. This was compared to the gold standard of "definite deaths". A comparative evaluation was also made of the time and costs associated with the two methods. RESULTS: Of the 450 definite deaths in our cohort the NDI correctly identified 417 and all of the 372 women known to be alive (sensitivity 93%, specificity 100%). Inconsistencies in identifiers recorded in our cohort files, particularly names, were responsible for the majority of known deaths not matching with the NDI, and if eliminated would increase the sensitivity to 98%. The cancer registries correctly identified 431 of the 450 definite deaths (sensitivity 96%). The costs associated with the NDI search were the same as the cancer registry searches, but the cancer registries took two months longer to conduct the searches. CONCLUSIONS AND IMPLICATIONS: This study indicates that the cancer registries are valuable, cost effective agencies for follow-up of mortality outcome in cancer cohorts, particularly where cohort members were residents of those states. For following large national cohorts the NDI provides additional information and flexibility when searching for deaths in Australia. This study also shows that women can be followed up for mortality with a high degree of accuracy using either service. Because each service makes a valuable contribution to the identification of deceased cancer subjects, both should be considered for optimal mortality follow-up in studies of cancer patients.

Art after 9/11

This article examines ways in which art can help broaden understandings of contemporary security challenges, especially in view of the limits of conventional forms of strategic and policy analysis. The article focuses especially on responses to 9/11 in literature, the visual arts, architecture, and music, and considers some epistemological questions about the status of art as a way of knowing political events, like those of 9/11, that escape state-based forms of security analysis.

Some economic dimensions of the mental health jigsaw in Australia

The purpose of this paper is to demonstrate that, although there are some unique features associated with mental illness, such special features do not preclude economic analysis. As a mechanism for understanding how individual economic studies fit into the mental health sector, a conceptual framework of the components of mental health service provision is outlined. Emphasis is placed on, not simply institutional and market resources, but also on the services provided by relatives, self-help groups, etc. Australian data on parts of the mental health sector are employed to illustrate that some (and different) economic analyses can be undertaken in mental health. First, time-series data on public psychiatric hospitals are employed to demonstrate trends associated with deinstitutionalisation. Other data (for Queensland alone) indicate that there are state-based differences in the provision of such services. Second, attention is then directed to the analysis of time-series data on private fee-for-service psychiatric services. Various concepts and measures from industrial economics are applied to analyse the relative size of this service industry, the pricing behaviour of the profession, the service-mix of "the psychiatry firms" operating in Australia.

Linear temporal logic and z refinement

Since Z, being a state-based language, describes a system in terms of its state and potential state changes, it is natural to want to describe properties of a specified system also in terms of its state. One means of doing this is to use Linear Temporal Logic (LTL) in which properties about the state of a system over time can be captured. This, however, raises the question of whether these properties are preserved under refinement. Refinement is observation preserving and the state of a specified system is regarded as internal and, hence, non-observable. In this paper, we investigate this issue by addressing the following questions. Given that a Z specification A is refined by a Z specification C, and that P is a temporal logic property which holds for A, what temporal logic property Q can we deduce holds for C? Furthermore, under what circumstances does the property Q preserve the intended meaning of the property P? The paper answers these questions for LTL, but the approach could also be applied to other temporal logics over states such as CTL and the mgr-calculus.

Abstract specification in Object-Z and CSP

A number of integrations of the state-based specification language Object-Z and the process algebra CSP have been proposed in recent years. In developing such integrations, a number of semantic decisions have to be made. In particular, what happens when an operation's precondition is not satisfied? Is the operation blocked, i.e., prevented from occurring, or can it occur with an undefined result? Also, are outputs from operations angelic, satisfying the environment's constraints on them, or are they demonic and not influenced by the environment at all? In this paper we discuss the differences between the models, and show that by adopting a blocking model of preconditions together with an angelic model of outputs one can specify systems at higher levels of abstraction.

High-pressure adsorption of supercritical gases on activated carbons: An improved approach based on the density functional theory and the bender equation of state

Adsorption of nitrogen, argon, methane, and carbon dioxide on activated carbon Norit R1 over a wide range of pressure (up to 50 MPa) at temperatures from 298 to 343 K (supercritical conditions) is analyzed by means of the density functional theory modified by incorporating the Bender equation of state, which describes the bulk phase properties with very high accuracy. It has allowed us to precisely describe the experimental data of carbon dioxide adsorption slightly above and below its critical temperatures. The pore size distribution (PSD) obtained with supercritical gases at ambient temperatures compares reasonably well with the PSD obtained with subcritical nitrogen at 77 K. Our approach does not require the skeletal density of activated carbon from helium adsorption measurements to calculate excess adsorption. Instead, this density is treated as a fitting parameter, and in all cases its values are found to fall into a very narrow range close to 2000 kg/m(3). It was shown that in the case of high-pressure adsorption of supercritical gases the PSD could be reliably obtained for the range of pore width between 0.6 and 3 run. All wider pores can be reliably characterized only in terms of surface area as their corresponding excess local isotherms are the same over a practical range of pressure.

Web services based state of the environment reporting

The Environmental Sciences Division within Queensland Environmental Protection Agency works to monitor, assess and model the condition of the environment. The Division has as a legislative responsibility to produce a whole-of-government report every four years dealing environmental conditions and trends in a ”State of the Environment report” (SoE)[1][2][3]. State of Environment Web Service Reporting System is a supplementary web service based SoE reporting tool, which aims to deliver accurate, timely and accessible information on the condition of the environment through web services via Internet [4][5]. This prototype provides a scientific assessment of environmental conditions for a set of environmental indicators. It contains text descriptions and tables, charts and maps with spatiotemporal dimensions to show the impact of certain environmental indicators on our environment. This prototype is a template based indicator system, to which the administrator may add new sql queries for new indicator services without changing the architecture and codes of this template. The benefits are brought through a service-oriented architecture which provides an online query service with seamless integration. In addition, since it uses web service architecture, each individual component within the application can be implemented by using different programming languages and in different operating systems. Although the services showed in this demo are built upon two datasets of regional ecosystem and protection area of Queensland, it will be possible to report on the condition of water, air, land, coastal zones, energy resources, biodiversity, human settlements and natural culture heritage on the fly as well. Figure 1 shows the architecture of the prototype. In the next section, I will discuss the research tasks in the prototype.

Numerical method for determination of the NMR frequency of the single-qubit operation in a silicon-based solid-state quantum computer

A numerical method is introduced to determine the nuclear magnetic resonance frequency of a donor (P-31) doped inside a silicon substrate under the influence of an applied electric field. This phosphorus donor has been suggested for operation as a qubit for the realization of a solid-state scalable quantum computer. The operation of the qubit is achieved by a combination of the rotation of the phosphorus nuclear spin through a globally applied magnetic field and the selection of the phosphorus nucleus through a locally applied electric field. To realize the selection function, it is required to know the relationship between the applied electric field and the change of the nuclear magnetic resonance frequency of phosphorus. In this study, based on the wave functions obtained by the effective-mass theory, we introduce an empirical correction factor to the wave functions at the donor nucleus. Using the corrected wave functions, we formulate a first-order perturbation theory for the perturbed system under the influence of an electric field. In order to calculate the potential distributions inside the silicon and the silicon dioxide layers due to the applied electric field, we use the multilayered Green's functions and solve an integral equation by the moment method. This enables us to consider more realistic, arbitrary shape, and three-dimensional qubit structures. With the calculation of the potential distributions, we have investigated the effects of the thicknesses of silicon and silicon dioxide layers, the relative position of the donor, and the applied electric field on the nuclear magnetic resonance frequency of the donor.