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.

User dyads in software testing: bypassing the need for expert observers

This paper arises out of a research study into the online help facilities provided in popular software applications such as word processors. Its particular focus is on experimental methods of evaluating the effectiveness and usability of those facilities. Focus groups, questionnaires, and online surveys had already been used in other phases of the study, but it was judged that these approaches would be unsuitable for measuring effectiveness and usability because they are susceptible to respondents' subjectivity. Direct observation of people working on set word-processing tasks was ruled out initially because of a lack of trained observers; it would have taken too long for the investigator to observe a large enough sample by himself. Automatic recording of users' actions was also rejected, as it would have demanded equipment and/or software that was not available and seemed too expensive to acquire. The approach and techniques described here were an attempt to overcome these difficulties by using observers drawn from the same population of students that provided the test subjects; as a by-product, this may also have enhanced the acceptability (and hence possibly the validity) of the experiments by reducing the exam pressure perceived by participants.

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.

Morphology of breast cancer as a means of triage of patients for BRCA1 genetic testing

Background: Women who have germline mutations in the BRCA1 gene are at substantially increased lifetime risk of developing breast and ovarian cancer but are otherwise normal. Currently. early age of onset of cancer and a strong family history are relied upon as the chief clues as to who should be offered genetic testing. Certain morphologic and immunohistochemical features are overrepresented in BRCA1-associated breast cancers but these differences have not been incorporated into the current selection criteria for genetic testing. Design: Each of the 4 pathologists studied 30 known cases of BRCA1- and BRCA2-associated breast cancer from kConFab families. After reviewing the literature, we agreed on a semiquantitative scoring system for estimating the chances of presence of an underlying BRCA1 mutation, based on the number of the reported prototypic features present. After a time lag of 12 months, we each examined a series of 62 deidentified cases of breast cancer, inclusive of cases of BRCA1-associated breast cancer and controls. The controls included cases of BRCA2-associated breast cancer and sporadic cases. Results: Our predictions had a sensitivity of 92%, specificity of 86%, positive predictive value of 61%, and negative predictive value of 98%. For comparison the sensitivity of currently used selection criteria are in the range of 25% to 30%. Conclusion: The inclusion of morphologic and immunohistochemical features of breast cancers in algorithms to predict the likelihood of presence of germline mutations in the BRCA1 gene improves the accuracy of the selection process.

Teaching principles of genetics through SNP analysis

An understanding of inheritance requires comprehension of genetic processes at all levels, from molecules to populations. Frequently genetics courses are separated into molecular and organismal genetics and students may fail to see the relationships between them. This is particularly true with human genetics, because of the difficulties in designing experimental approaches which are consistent with ethical restrictions, student abilities and background knowledge, and available time and materials. During 2005 we used analysis of single nucleotide polymorphisms (SNPs) in two genetic regions to enhance student learning and provide a practical experience in human genetics. Students scanned databases to discover SNPs in a gene of interest, used software to design PCR primers and a restriction enzyme based assay for the alleles, and carried out an analysis of the SNP on anonymous individual and family DNAs. The project occupied eight to ten hours per week for one semester, with some time spent in the laboratory and some spent in database searching, reading and writing the report. In completing their projects, students acquired a knowledge of Mendel’s first law (through looking at inheritance patterns), Mendel’s second law and the exceptions (the concepts of linkage and linkage disequilibrium), DNA structure (primer design and restriction enzyme analysis) and function (SNPs in coding and non-coding regions), population genetics and the statistical analysis of allele frequencies, genomics, bioinformatics and the ethical issues associated with the use of human samples. They also developed skills in presentation of results by publication and conference participation. Deficiencies in their understanding (for example of inheritance patterns, gene structure, statistical approaches and report writing) were detected and guidance given during the project. SNP analysis was found to be a powerful approach to enhance and integrate student understanding of genetic concepts.

Ethics and intervention: The 'humanitarian exception' and the problem of abuse in the case of Iraq

This article investigates the ethics of intervention and explores the decision to invade Iraq. It begins by arguing that while positive international law provides an important framework for understanding and debating the legitimacy of war, it does not cover the full spectrum of moral reasoning on issues of war and peace. To that end, after briefly discussing the two primary legal justifications for war (implied UN authorization and pre-emptive self-defence), and finding them wanting, it asks whether there is a moral 'humanitarian exceptions to this rule grounded in the 'just war' tradition. The article argues that two aspects of the broad tradition could be used to make a humanitarian case for war: the 'holy war' tradition and classical just war thinking based on natural law. The former it finds problematic, while the latter it argues provides a moral space to justify the use of force to halt gross breaches of natural law. Although such an approach may provide a moral justification for war, it also opens the door to abuse. It was this very problem that legal positivism from Vattel onwards was designed to address. As a result, the article argues that natural law and legal positivist arguments should be understood as complementary sets of ideas whose sometimes competing claims must be balanced in relation to particular cases. Therefore, although natural law may open a space for justifying the invasion of Iraq on humanitarian terms, legal positivism strictly limits that right. Ignoring this latter fact, as happened in the Iraq case, opens the door to abuse.

The implications of simultaneous smoking initiation for inferences about the genetics of smoking behavior from twin data

We examined early social influences across stages of smoking within the context of a twin study using an environmental exposure specific to smoking: whether twins started smoking at the same time (simultaneous smoking initiation: SSI). We expected that SSI would be a good index of shared social influences on smoking initiation. Rates of SSI were indeed significantly higher in MZ twins and in twins who shared peers and classes, as well as in male twins. With the exception of regular smoking in females, we found no significant difference in estimates of genetic and environmental parameters between SSI and non-SSI pairs for any of the smoking measures that we examined (DSM-IV and Fagerstrom HSI measures of nicotine dependence; DSM-IV nicotine withdrawal; heavy smoking; and in males, regular smoking). For regular smoking in females, allowing for additional shared environmental influences associated with SSI only modestly reduced our estimates of additive genetic variance (56% vs. 68%). These results indicate the important social influences that may occur for smoking initiation do not appear to seriously bias estimates of genetic effects on later stages of smoking.

Managing change and time in dynamic workflow processes

Business environments have become exceedingly dynamic and competitive in recent times. This dynamism is manifested in the form of changing process requirements and time constraints. Workflow technology is currently one of the most promising fields of research in business process automation. However, workflow systems to date do not provide the flexibility necessary to support the dynamic nature of business processes. In this paper we primarily discuss the issues and challenges related to managing change and time in workflows representing dynamic business processes. We also present an analysis of workflow modifications and provide feasibility considerations for the automation of this process.

Refining exceptions using King and Morgan's exit construct

In this paper we discuss the refinement of exceptions. We extend the Guarded Command Language normally used in the refinement calculus, with a simple exception handling statement, which we model using King and Morgan's exit statement (1995). We derive some variants of King and Morgan's refinement laws for their exit statement, and illustrate the approach with an example of a refinement of a simple program.