A formal model of real-time program compilation

Program compilation can be formally defined as a sequence of equivalence-preserving transformations, or refinements, from high-level language programs to assembler code, Recent models also incorporate timing properties, but the resulting formalisms are intimidatingly complex. Here we take advantage of a new, simple model of real-time refinement, based on predicate transformer semantics, to present a straightforward compilation formalism that incorporates real-time constraints. (C) 2002 Elsevier Science B.V. All rights reserved.

The variety of variables in automated real-time refinement

The refinement calculus is a well-established theory for deriving program code from specifications. Recent research has extended the theory to handle timing requirements, as well as functional ones, and we have developed an interactive programming tool based on these extensions. Through a number of case studies completed using the tool, this paper explains how the tool helps the programmer by supporting the many forms of variables needed in the theory. These include simple state variables as in the untimed calculus, trace variables that model the evolution of properties over time, auxiliary variables that exist only to support formal reasoning, subroutine parameters, and variables shared between parallel processes.

An SNP-based PCR assay to differentiate between Listeria monocytogenes lineages derived from phylogenetic analysis of the sigB gene

The alternative sigma factor sigB gene is involved in the stress response regulation of Listeria monocytogenes, and contributes towards growth and survival in adverse conditions. This gene was examined to determine if it could be a useful indicator of lineage differentiation, similar to the established method based on ribotyping. The sigB sequence was resolved in four local L. monocytogenes strains and the phylogenetic relationship among these, and a further 21 sigB gene sequences from strains of different serotype and lineage including two Listeria innocua strains, obtained from the GenBank database were determined. The sigB nucleotide sequences of these 25 Listeria strains were then examined for single nucleotide polymorphic (SNP) sites that could differentiate between the three lineages. Based on nucleotide sequences L. monocytogenes lineage F serotype 1/2b and 4b clustered together, lineage II/serotype 1/2a and 1/2c strains clustered together, lineage III/serotypes 4a and 4c strains clustered together and L. innocua strains clustered together as an outgroup. SNPs differentiating the three lineages were identified. Individual allele-specific PCR reactions based on these polymorphisms were successful in grouping known and a further 37 local L. monocytogenes isolates into the three lineages. (C) 2003 Elsevier B.V. All fights reserved.