Determining the specification of a control system from that of its environment

Well understood methods exist for developing programs from given specifications. A formal method identifies proof obligations at each development step: if all such proof obligations are discharged, a precisely defined class of errors can be excluded from the final program. For a class of closed systems such methods offer a gold standard against which less formal approaches can be measured. For open systems -those which interact with the physical world- the task of obtaining the program specification can be as challenging as the task of deriving the program. And, when a system of this class must tolerate certain kinds of unreliability in the physical world, it is still more challenging to reach confidence that the specification obtained is adequate. We argue that widening the notion of software development to include specifying the behaviour of the relevant parts of the physical world gives a way to derive the specification of a control system and also to record precisely the assumptions being made about the world outside the computer.

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.

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.

Supporting the software testing process through specification animation

Achieving consistency between a specification and its implementation is an important part of software development. In this paper, we present a method for generating passive test oracles that act as self-checking implementations. The implementation is verified using an animation tool to check that the behavior of the implementation matches the behavior of the specification. We discuss how to integrate this method into a framework developed for systematically animating specifications, which means a tester can significantly reduce testing time and effort by reusing work products from the animation. One such work product is a testgraph: a directed graph that partially models the states and transitions of the specification. Testgraphs are used to generate sequences for animation, and during testing, to execute these same sequences on the implementation.

Integrating runtime assertions with dynamic types: Structuring a derivation from an incomputable specification

An inherent incomputability in the specification of a functional language extension that combines assertions with dynamic type checking is isolated in an explicit derivation from mathematical specifications. The combination of types and assertions (into "dynamic assertion-types" - DATs) is a significant issue since, because the two are congruent means for program correctness, benefit arises from their better integration in contrast to the harm resulting from their unnecessary separation. However, projecting the "set membership" view of assertion-checking into dynamic types results in some incomputable combinations. Refinement of the specification of DAT checking into an implementation by rigorous application of mathematical identities becomes feasible through the addition of a "best-approximate" pseudo-equality that isolates the incomputable component of the specification. This formal treatment leads to an improved, more maintainable outcome with further development potential.

Bellerophon: a program to detect chimeric sequences in multiple sequence alignments

Bellerophon is a program for detecting chimeric sequences in multiple sequence datasets by an adaption of partial treeing analysis. Bellerophon was specifically developed to detect 16S rRNA gene chimeras in PCR-clone libraries of environmental samples but can be applied to other nucleotide sequence alignments.

Combining GIS and Expert Opinion to Model Landscapes for a Smallholder Forest Extension Program in Leyte, the Philippines

A Geographic Information System (GIS) was used to model datasets of Leyte Island, the Philippines, to identify land which was suitable for a forest extension program on the island. The datasets were modelled to provide maps of the distance of land from cities and towns, land which was a suitable elevation and slope for smallholder forestry and land of various soil types. An expert group was used to assign numeric site suitabilities to the soil types and maps of site suitability were used to assist the selection of municipalities for the provision of extension assistance to smallholders. Modelling of the datasets was facilitated by recent developments of the ArcGIS® suite of computer programs and derivation of elevation and slope was assisted by the availability of digital elevation models (DEM) produced by the Shuttle Radar Topography (SRTM) mission. The usefulness of GIS software as a decision support tool for small-scale forestry extension programs is discussed.

An evaluation of the Keep on Talking program for maintaining communication skills into old

Communication skills change with age as a result of sensory deficits, memory loss, and increasing word finding difficulties The Keep on Talking program (L. Hickson, H. Barnett, L. Worrall, & E. Yiu, 1994) was developed to assist older people to develop their own strategies for maintaining communication skills into old age. Two hundred and fifty-two healthy older people were recruited from the community and were assessed on a battery of communication assessments on entry to the study and at 1 year after entry. The experimental group (n = 120) participated in the 5-week group Keep on Talking program run by volunteers A further 130 control subjects were assessed only. The short-term effectiveness of the program was evaluated using a short knowledge based and attitudinal questionnaire and qualitative written feedback. At the I-year follow up, subjects were also asked whether they had taken any action as a result of the project. Results concluded that there was a significant difference between the number of correct questionnaire responses on the knowledge based items and the ratings on the attitudinal items pre- and postprogram questionnaire for the experimental subjects. Qualitative written feedback was positive with many participants remarking on the amount of information that they had acquired. Forty-eight experimental and 69 control subjects (n = 117) were assessed I year later, and there was a significant difference between the groups in terms of the number of subjects who reported having taken action as a result of the program. The Keep on Talking program increased knowledge about communication, produced a positive change in attitude toward the importance of communication, and encouraged participants to take action to maintain their communication skills. Maintaining communication skills may prevent social isolation. This simple 5-hour group program has been effective in empowering participants to maintain. their communication skills as they age.

Interval breast cancers in an Australian mammographic screening program

Objective: To determine the incidence of interval cancers which occurred in the first 12 months after mammographic screening at a mammographic screening service. Design: Retrospective analysis of data obtained by crossmatching the screening Service and the New South Wales Central Cancer Registry databases. Setting: The Central & Eastern Sydney Service of BreastScreen NSW. Participants: Women aged 40-69 years at first screen, who attended for their first or second screen between 1 March 1988 and 31 December 1992. Main outcome measures: Interval-cancer rates per 10 000 screens and as a proportion of the underlying incidence of breast cancer (as estimated by the underlying rate in the total NSW population). Results: The 12-month interval-cancer incidence per 10 000 screens was 4.17 for the 40-49 years age group (95% confidence interval [CI], 1.35-9.73) and 4.64 for the 50-69 years age group (95% CI, 2.47-7.94). Proportional incidence rates were 30.1% for the 40-49 years age group (95% CI, 9.8-70.3) and 22% for the 50-69 years age group (95% CI, 11.7-37.7). There was no significant difference between the proportional incidence rate for the 50-69 years age group for the Central & Eastern Sydney Service and those of major successful overseas screening trials. Conclusion: Screening quality was acceptable and should result in a significant mortality reduction in the screened population. Given the small number of cancers involved, comparison of interval-cancer statistics of mammographic screening programs with trials requires age-specific or age-adjusted data, and consideration of confidence intervals of both program and trial data.

A bleach program for inmates in NSW: an HIV prevention strategy

Syringe cleaning guidelines for injecting drug users (IDUs) were revised in 1993. This paper examines efforts by IDUs in NSW prisons to adopt the revised guidelines in 1994. Consecutive inmates (229) nearing release were visited and asked to call a toll free number for an interview once released. Respondents (102) did not differ from non-respondents (127). Many respondents (64%) reported ever injecting and many of these reported injecting (58%), sharing (48%) and syringe cleaning (46%) when last in prison. Some (23%) respondents reported adopting the revised syringe cleaning guidelines. Tattooing (38%) was reported more often than sexual activity in prison (4%). A new methodology for prison research was found to be feasible in this study. The potential for HIV to spread in prison still poses major public health challenges.

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.

Effects of a program of intervention on parental distress following infant death

A longitudinal study of 144 patents (65 fathers, 79 mothers) was conducted to evaluate the effectiveness of a program of intervention in relieving the psychological distress of parents affected by infant death. Participants were assessed in terms of their psychiatric disturbance, depression, anxiety, physical symptoms, dyadic adjustment, and coping strategies. The experimental group (n = 84) was offered an intervention program comprising the use of specially designed resources and contact with a trained grief worker. A control group (n = 60) was given routine community care. Parental reactions were assessed at four to six weeks postloss (prior to the implementation of the intervention program), at six months postloss, and at 15 months postloss. A series of multivariate analyses of valiance revealed that the intervention was effective in reducing the distress of parents, particularly those assessed prior to the intervention as being at high-risk of developing mourning difficulties. Effects of the intervention were noted in terms of parents' overall psychiatric disturbance, marital quality, and paternal coping strategies.

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.