The real-time refinement calculus: A foundation for machine-independent real-time programming

The real-time refinement calculus is an extension of the standard refinement calculus in which programs are developed from a precondition plus post-condition style of specification. In addition to adapting standard refinement rules to be valid in the real-time context, specific rules are required for the timing constructs such as delays and deadlines. Because many real-time programs may be nonterminating, a further extension is to allow nonterminating repetitions. A real-time specification constrains not only what values should be output, but when they should be output. Hence for a program to implement such a specification, it must guarantee to output values by the specified times. With standard programming languages such guarantees cannot be made without taking into account the timing characteristics of the implementation of the program on a particular machine. To avoid having to consider such details during the refinement process, we have extended our real-time programming language with a deadline command. The deadline command takes no time to execute and always guarantees to meet the specified time; if the deadline has already passed the deadline command is infeasible (miraculous in Dijkstra's terminology). When such a realtime program is compiled for a particular machine, one needs to ensure that all execution paths leading to a deadline are guaranteed to reach it by the specified time. We consider this checking as part of an extended compilation phase. The addition of the deadline command restores for the real-time language the advantage of machine independence enjoyed by non-real-time programming languages.

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.

Reasoning about timeouts

In real-time programming a timeout mechanism allows exceptional behaviour, such as a lack of response, to be handled effectively, while not overly affecting the programming for the normal case. For. example, in a pump controller if the water level has gone below the minimum level and the pump is on and hence pumping in more water, then the water level should rise above the minimum level within a specified time. If not, there is a fault in the system and it should be shut down and an alarm raised. Such a situation can be handled by normal case code that determines when the level has risen above the minimum, plus a timeout case handling the situation when the specified time to reach the minimum has passed. In this paper we introduce a timeout mechanism, give it a formal definition in terms of more basic real-time commands, develop a refinement law for introducing a timeout clause to implement a specification, and give an example of using the law to introduce a timeout. The framework used is a machine-independent real-time programming language, which makes use of a deadline command to represent timing constraints in a machine-independent fashion. This allows a more abstract approach to handling timeouts.

Towards a refinement calculus for concurrent real-time programs

We define a language and a predicative semantics to model concurrent real-time programs. We consider different communication paradigms between the concurrent components of a program: communication via shared variables and asynchronous message passing (for different models of channels). The semantics is the basis for a refinement calculus to derive machine-independent concurrent real-time programs from specifications. We give some examples of refinement laws that deal with concurrency.

Reasoning about deadlines in concurrent real-time programs

We propose a method for the timing analysis of concurrent real-time programs with hard deadlines. We divide the analysis into a machine-independent and a machine-dependent task. The latter takes into account the execution times of the program on a particular machine. Therefore, our goal is to make the machine-dependent phase of the analysis as simple as possible. We succeed in the sense that the machine-dependent phase remains the same as in the analysis of sequential programs. We shift the complexity introduced by concurrency completely to the machine-independent phase.

Human behaviour modelled as a statistico-deterministic turing machine

'Free will' and its corollary, the concept of individual responsibility are keystones of the justice system. This paper shows that if we accept a physics that disallows time reversal, the concept of 'free will' is undermined by an integrated understanding of the influence of genetics and environment on human behavioural responses. Analysis is undertaken by modelling life as a novel statistico-deterministic version of a Turing machine, i.e. as a series of transitions between states at successive instants of time. Using this model it is proven by induction that the entire course of life is independent of the action of free will. Although determined by prior state, the probability of transitions between states in response to a standard environmental stimulus is not equal to 1 and the transitions may differ quantitatively at the molecular level and qualitatively at the level of the whole organism. Transitions between states correspond to behaviours. It is shown that the behaviour of identical twins (or clones), although determined, would be incompletely predictable and non-identical, creating an illusion of the operation of 'free will'. 'Free will' is a convenient construct for current judicial systems and social control because it allows rationalization of punishment for those whose behaviour falls outside socially defined norms. Indeed, it is conceivable that maintenance of ideas of free will has co-evolved with community morality to reinforce its operation. If the concept is free will is to be maintained it would require revision of our current physical theories.

Evolutionary conservation of the membrane fusion machine

Recent structural studies of proteins mediating membrane fusion reveal intriguing similarities between diverse viral and mammalian systems. Particularly striking is the close similarity between the transmembrane envelope glycoproteins from the retrovirus HTLV-1 and the filovirus Ebola. These similarities suggest similar mechanisms of membrane fusion. The model that fits most currently available data suggests fusion activation in viral systems is driven by a symmetrical conformational change triggered by an activation event such as receptor binding or a pH change. The mammalian vesicle fusion mediated by the SNARE protein complex most likely occurs by a similar mechanism but without symmetry constraints.

Myb-binding Protein 1a is a Nucleocytoplasmic Shuttling Protein that Utilizes CRM1-dependent and Independent Nuclear Export Pathways

Myb-binding protein 1a (Mybbp1a) is a novel nuclear protein localized predominantly, but not exclusively, in nucleoli. Although initially isolated as a c-Myb interacting protein, Mybbp1a is expressed ubiquitously, associates with a number of different transcription factors, and may play a role in both RNA polymerase I- and II-mediated transcriptional regulation. However, its precise function remains unclear. In this study we show that Mybbp1a is a nucleocytoplasmic shuttling protein and investigate the mechanisms responsible for both nuclear import and export. The carboxyl terminus of Mybbp1a, which contains seven short basic amino acid repeat sequences, is responsible for both nuclear and nucleolar localization, and this activity can be transferred to a heterologous protein. Deletion mapping demonstrated that these repeat sequences appear to act incrementally, with successive deletions resulting in a corresponding increase in the proportion of protein localized in the cytoplasm. Glutathione S-transferase pulldown experiments showed that the nuclear receptor importin-alpha/beta mediates Mybbp1a nuclear import. Interspecies heterokaryons were used to demonstrate that Mybbp1a was capable of shuttling between the nucleus and the cytoplasm. Deletion analysis and in vivo export studies using a heterologous assay system identified several nuclear export sequences which facilitate Mybbp1a nuclear export of Mybbp1a by CRM1-dependent and -independent pathways. (C) 2003 Elsevier Science (USA). All rights reserved.

A study of the interaction between operator style and machine capability for a hydraulic mining excavator

This paper presents a case study that explores how operator digging style juxtaposes with mechanical capability for a class of hydraulic mining excavators. The relationships between actuator and digging forces are developed and these are used to identify the excavator's capability to apply forces in various directions. Two distinct modes of operation are examined to see how they relate to the mechanical capabilities of the linkage and to establish if one has merit over the other. It is found that one of these styles results in lower loading of the machine.

DNA binding-independent transcriptional activation of the vascular endothelial growth factor gene (VEGF) by the Myb oncoprotein

Myb is a key transcription factor that can regulate proliferation, differentiation, and apoptosis, predominantly in the haemopoietic system. Abnormal expression of Myb is associated with a number of cancers, both haemopoietic and non-haemopoietic. In order to better understand the role of Myb in normal and tumorigenic processes, we undertook a cDNA array screen to identify genes that are regulated by this factor. In this way, we identified the gene encoding vascular endothelial growth factor (VEGF) as being potentially regulated by the Myb oncoprotein in myeloid cells. To determine whether this was a direct effect on VEGF gene transcription, we examined the activity of the murine VEGF promoter in the presence of either wild-type (WT) or mutant forms of Myb. It was found that WT Myb was able to activate the VEGF promoter and that a minimal promoter region of 120 bp was sufficient to confer Myb responsiveness. Surprisingly, activation of the VEGF promoter was independent of DNA binding by Myb. This was shown by the use of DNA binding-defective Myb mutants and by mutagenesis of a potential Myb-binding site in the minimal promoter. Mutation of Sp1 sites within this region abolished Myb-mediated regulation of a reporter construct, suggesting that Myb DNA binding-independent activation of VEGF expression occurs via these Sp1 binding elements. Regulation of VEGF production by Myb has implications for the potential role of Myb in myeloid leukaemias and in solid tumours where VEGF may be functioning as an autocrine growth factor. (c) 2006 Elsevier Inc. All rights reserved.

Evidence that two independent host genes influence the severity of tissue damage and susceptibility to acute pyelonephritis in murine systemic candidiasis

Tissue damage in the kidney and brain after systemic infection with Candida albicans was examined in recombinant inbred strains (AKXL) derived from AKR and C57/L progenitors. Nine of the 15 strains showed mild (C57/L-like) tissue damage. Of the remainder, two strains developed lesions comparable to the AKR parental strain, whereas four exhibited a much move severe pattern of tissue damage. This was characterized by pronounced mycelial growth in the brain, and gross oedema of the kidney, with extensive fungal colonization and marked tissue destruction. The presence of the null allele of the haemolytic complement gene (Hc) may be necessary but not sufficient, for the expression of the very severe lesions. The results were interpreted as reflecting the actions of two independent genes, which have been designated Carg1 and Carg2 (Candida albicans resistance genes 1 and 2). (C) 1997 Academic Press Limited.

Expression of activated mutants of the human interleukin-3/interleukin-5 granulocyte-macrophage colony-stimulating factor receptor common beta subunit in primary hematopoietic cells induces factor-independent proliferation and differentiation

To date, several activating mutations have been discovered in the common signal-transducing subunit (h beta c) of the receptors for human granulocyte-macrophage colony-stimulating factor, interleukin-3, and interleukin-5. Two of these, Fl Delta and 1374N, result in a 37 amino acid duplication and a single amino acid substitution in the extracellular domain of h beta c, respectively. A third, V449E, results in a single amino acid substitution in the transmembrane domain, Previous studies comparing the activity of these mutants in different hematopoietic cell lines imply that the transmembrane and extracellular mutations act by different mechanisms and suggest the requirement for cell type-specific molecules in signalling. To characterize the ability of these mutant hpc subunits to mediate growth and differentiation of primary cells and hence investigate their oncogenic potential, we have expressed all three mutants in primary murine hematopoietic cells using retroviral transduction. It is shown that, whereas expression of either extracellular hpc mutant confers factor-independent proliferation and differentiation on cells of the neutrophil and monocyte lineages only, expression of the transmembrane mutant does so on these lineages as well as the eosinophil, basophil, megakaryocyte, and erythroid lineages, Factor-independent myeloid precursors expressing the transmembrane mutant display extended proliferation in liquid culture and in some cases yielded immortalized cell lines. (C) 1997 by The American Society of Hematology.