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.

A framework for specification-based testing

Test templates and a test template framework are introduced as useful concepts in specification-based testing. The framework can be defined using any model-based specification notation and used to derive tests from model-based specifications-in this paper, it is demonstrated using the Z notation. The framework formally defines test data sets and their relation to the operations in a specification and to other test data sets, providing structure to the testing process. Flexibility is preserved, so that many testing strategies can be used. Important application areas of the framework are discussed, including refinement of test data, regression testing, and test oracles.

Structural refinement of systems specified in object-z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.

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.

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.

Dietary influences on survival after ovarian cancer

We evaluated the effects of various food groups and micronutrients in the diet on survival among women who originally participated in a population-based case-control study of ovarian cancer conducted across 3 Australian states between 1990 and 1993. This analysis included 609 women with invasive epithelial ovarian cancer, primarily because there was negligible mortality in women with borderline tumors. The women's usual diet was assessed using a validated food frequency questionnaire. Deaths in the cohort were identified using state-based cancer registries and the Australian National Death Index (NDI). Crude 5-year survival probabilities were estimated using the Kaplan-Meier technique, and adjusted hazard ratios (HRs) and 95% confidence intervals (CIs) were obtained from Cox regression models. After adjusting for important confounding factors, a survival advantage was observed for those who reported higher intake of vegetables in general (HR = 0.75, 95% CI = 0.57-0.99, p-value trend 0.01 for the highest third, compared to the lowest third), and cruciferous vegetables in particular (HR = 0.75, 95% CI = 0.57-0.98, p-value trend 0.03), and among women in the upper third of intake of vitamin E (HR = 0.76, 95% CI = 0.58-1.01, p-value trend 0.04). Inverse associations were also seen with protein (p-value trend 0.09), red meat (p-value trend 0.06) and white meat (p-value trend 0.07), and modest positive trends (maximum 30% excess) with lactose (p-value trend 0.04), calcium and dairy products. Although much remains to be learned about the influence of nutritional factors after a diagnosis of ovarian cancer, our study suggests the possibility that a diet high in vegetable intake may help improve survival. (C) 2003 Wiley-Liss, Inc.

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.