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.

Interfacing ASM with the MDG tool

In this paper we describe an approach to interface Abstract State Machines (ASM) with Multiway Decision Graphs (MDG) to enable tool support for the formal verification of ASM descriptions. ASM is a specification method for software and hardware providing a powerful means of modeling various kinds of systems. MDGs are decision diagrams based on abstract representation of data and axe used primarily for modeling hardware systems. The notions of ASM and MDG axe hence closely related to each other, making it appealing to link these two concepts. The proposed interface between ASM and MDG uses two steps: first, the ASM model is transformed into a flat, simple transition system as an intermediate model. Second, this intermediate model is transformed into the syntax of the input language of the MDG tool, MDG-HDL. We have successfully applied this transformation scheme on a case study, the Island Tunnel Controller, where we automatically generated the corresponding MDG-HDL models from ASM specifications.

Effect of sequence variation in Plasmodium falciparum Histidine-Rich protein 2 on binding of specific monoclonal antibodies: Implications for rapid diagnostic tests for malaria

This Article Right arrow Full Text Right arrow Full Text (PDF) Right arrow Supplemental material Right arrow Alert me when this article is cited Right arrow Alert me if a correction is posted Services Right arrow Similar articles in this journal Right arrow Similar articles in PubMed Right arrow Alert me to new issues of the journal Right arrow Download to citation manager Right arrow Reprints and Permissions Right arrow Copyright Information Right arrow Books from ASM Press Right arrow MicrobeWorld Citing Articles Right arrow Citing Articles via HighWire Right arrow Citing Articles via Google Scholar Google Scholar Right arrow Articles by Lee, N. Right arrow Articles by McCarthy, J. Right arrow Search for Related Content PubMed Right arrow PubMed Citation Right arrow Articles by Lee, N. Right arrow Articles by McCarthy, J. Right arrow Pubmed/NCBI databases * Substance via MeSH Previous Article | Next Article Journal of Clinical Microbiology, August 2006, p. 2773-2778, Vol. 44, No. 8 0095-1137/06/$08.00+0 doi:10.1128/JCM.02557-05 Copyright © 2006, American Society for Microbiology. All Rights Reserved. Effect of Sequence Variation in Plasmodium falciparum Histidine- Rich Protein 2 on Binding of Specific Monoclonal Antibodies: Implications for Rapid Diagnostic Tests for Malaria{dagger} Nelson Lee,1,2 Joanne Baker,2 Kathy T. Andrews,1 Michelle L. Gatton,1,3 David Bell,4 Qin Cheng,2,3 and James McCarthy1* Australian Centre for International and Tropical Health and Nutrition, Queensland Institute of Medical Research and School of Population Health, University of Queensland, Queensland, Australia,1 Department of Drug Resistance and Diagnostics, Australian Army Malaria Institute, Brisbane, Australia,2 Malaria Drug Resistance and Chemotherapy, Queensland Institute of Medical Research, Queensland, Australia,3 World Health Organization, Regional Office for the Western Pacific, Manila, Philippines4 Received 8 December 2005/ Returned for modification 23 February 2006/ Accepted 26 May 2006 The ability to accurately diagnose malaria infections, particularly in settings where laboratory facilities are not well developed, is of key importance in the control of this disease. Rapid diagnostic tests (RDTs) offer great potential to address this need. Reports of significant variation in the field performance of RDTs based on the detection of Plasmodium falciparum histidine-rich protein 2 (HRP2) (PfHRP2) and of significant sequence polymorphism in PfHRP2 led us to evaluate the binding of four HRP2-specific monoclonal antibodies (MABs) to parasite proteins from geographically distinct P. falciparum isolates, define the epitopes recognized by these MABs, and relate the copy number of the epitopes to MAB reactivity. We observed a significant difference in the reactivity of the same MAB to different isolates and between different MABs tested with single isolates. When the target epitopes of three of the MABs were determined and mapped onto the peptide sequences of the field isolates, significant variability in the frequency of these epitopes was observed. These findings support the role of sequence variation as an explanation for variations in the performance of HRP2-based RDTs and point toward possible approaches to improve their diagnostic sensitivities

Acibenzolar-S-methyl and methyl jasmonate treatments of glasshouse-grown freesias suppress post-harvest petal specking caused by Botrytis cinerea

Compounds that activate host plant defence responses potentially offer socio-environmentally sound alternative methods for disease control. In a series of glasshouse trials over 2 years, pre-harvest sprays with acibenzolar-S-methyl (ASM) and methyl jasmonate (MeJA) were tested for suppression of post-harvest infection of cut Freesia hybrida L. flowers by Botrytis cinerea. For the ASM treatments, variability in reducing the incidence of B. cinerea disease was observed between years freesia varieties, incubation temperatures and ASM concentrations. In the first year, the greatest reductions in lesion numbers on ASM-treated var. 'Cote d'Azur' were recorded using 2.86 mM ASM. For three different post-harvest temperature regimes, the relative reductions in lesion numbers, compared to untreated controls, were 45% at 5 degrees C, 40% at 12 degrees C and 30% at 20 degrees C, respectively. In the second year, lesion numbers were most reduced using 1.43 mM ASM to treat freesia var. 'Dukaat' flowers. Here, the relative reductions were to 44% at 5 degrees C, 26% at 12 degrees C and 51% at 20 degrees C. MeJA treatments were, in general, more consistently effective than ASM treatments in reducing lesion numbers and lesion diameters on cut freesia flowers. MeJA-treated (0.2 mM) freesia flowers (var. 'Dukaat') incubated at 20 degrees C showed relative reductions of 62%, and 45% for lesion number and lesion diameter, respectively. The differing efficacy between ASM and MeJA treatments could be attributed to their differential abilities to induce the salicylic acid (SA)-mediated vs. the jasmonic acid (JA)-mediated host defence pathways, respectively.

Automatic segmentation of the knee bones using 3D active shape models

This paper presents an automated segmentation approach for MR images of the knee bones. The bones are the first stage of a segmentation system for the knee, primarily aimed at the automated segmentation of the cartilages. The segmentation is performed using 3D active shape models (ASM), which are initialized using an affine registration to an atlas. The 3D ASMs of the bones are created automatically using a point distribution model optimization scheme. The accuracy and robustness of the segmentation approach was experimentally validated using an MR database of fat suppressed spoiled gradient recall images.