Functional analysis of a real-time protocol for networked control systems

Traditional real-time control systems are tightly integrated into the industrial processes they govern. Now, however, there is increasing interest in networked control systems. These provide greater flexibility and cost savings by allowing real-time controllers to interact with industrial processes over existing communications networks. New data packet queuing protocols are currently being developed to enable precise real-time control over a network with variable propagation delays. We show how one such protocol was formally modelled using timed automata, and how model checking was used to reveal subtle aspects of the control system's dynamic behaviour.

Structured ontology and information retrieval for email search and discovery

This paper discusses an document discovery tool based on formal concept analysis. The program allows users to navigate email using a visual lattice metaphor rather than a tree. It implements a virtual file structure over email where files and entire directories can appear in multiple positions. The content and shape of the lattice formed by the conceptual ontology can assist in email discovery. The system described provides more flexibility in retrieving stored emails than what is normally available in email clients. The paper discusses how conceptual ontologies can leverage traditional document retrieval systems.

Are echo techniques comparable for measurement of left ventricular dysynchrony? Comparison of real time 3D and tissue Doppler echocardiography in patients with ischaemic cardiomyopathy

Tissue Doppler (TD) assessment of dysynchrony (DYS) is established in evaluation for bi-ventricular pacing. Time to regional minimal volume by real-time 3D echo (3D) has been applied to DYS. 3D offers simultaneous assessment of all segments and may limit errors in localization of maximum delay due to off-axis images.We compared TD and 3D for assessment of DYS. 27 patients with ischaemic cardiomyopathy (aged 60±11 years, 85% male) underwent TD with generation of regional velocity curves. The interval between QRS onset and maximal systolic velocity (TTV) was measured in 6 basal and 6 mid-cavity segments. Onthe same day,3Dwas performed and data analysed offline with Q-Lab software (Philips, Andover, MA). Using 12 analogous regional time-volume curves time to minimal volume (T3D)was calculated. The standard deviation (S.D.) between segments in TTV and T3D was calculated as a measure ofDYS. In 7 patients itwas not possible to measureT3D due to poor images. In the remaining 20, LV diastolic volume, systolic volume and EF were 128±35 ml, 68±23 ml and 46±13%, respectively. Mean TTV was less than mean T3D (150±33ms versus 348±54 ms; p < 0.01). The intrapatient range was 20–210ms for TTV and 0–410ms for T3D. Of 9 patients (45%) with significantDYS (S.D. TTV > 32 ms), S.D. T3D was 69±37ms compared to 48±34ms in those without DYS (p = ns). In DYS patients there was concordance of the most delayed segment in 4 (44%) cases.Therefore, different techniques for assessing DYS are not directly comparable. Specific cut-offs for DYS are needed for each technique.

A theory for execution-time derivation in real-time programs

We provide an abstract command language for real-time programs and outline how a partial correctness semantics can be used to compute execution times. The notions of a timed command, refinement of a timed command, the command traversal condition, and the worst-case and best-case execution time of a command are formally introduced and investigated with the help of an underlying weakest liberal precondition semantics. The central result is a theory for the computation of worst-case and best-case execution times from the underlying semantics based on supremum and infimum calculations. The framework is applied to the analysis of a message transmitter program and its implementation. (c) 2005 Elsevier B.V. All rights reserved.

Termination of real-time programs: Definitely, definitely not, or maybe

Real-time control programs are often used in contexts where (conceptually) they run forever. Repetitions within such programs (or their specifications) may either (i) be guaranteed to terminate, (ii) be guaranteed to never terminate (loop forever), or (iii) may possibly terminate. In dealing with real-time programs and their specifications, we need to be able to represent these possibilities, and define suitable refinement orderings. A refinement ordering based on Dijkstra's weakest precondition only copes with the first alternative. Weakest liberal preconditions allow one to constrain behaviour provided the program terminates, which copes with the third alternative to some extent. However, neither of these handles the case when a program does not terminate. To handle this case a refinement ordering based on relational semantics can be used. In this paper we explore these issues and the definition of loops for real-time programs as well as corresponding refinement laws.

An agent-based approach to modelling driver route choice behaviour under the influence of real-time information

This paper presents an agent-based approach to modelling individual driver behaviour under the influence of real-time traffic information. The driver behaviour models developed in this study are based on a behavioural survey of drivers which was conducted on a congested commuting corridor in Brisbane, Australia. Commuters' responses to travel information were analysed and a number of discrete choice models were developed to determine the factors influencing drivers' behaviour and their propensity to change route and adjust travel patterns. Based on the results obtained from the behavioural survey, the agent behaviour parameters which define driver characteristics, knowledge and preferences were identified and their values determined. A case study implementing a simple agent-based route choice decision model within a microscopic traffic simulation tool is also presented. Driver-vehicle units (DVUs) were modelled as autonomous software components that can each be assigned a set of goals to achieve and a database of knowledge comprising certain beliefs, intentions and preferences concerning the driving task. Each DVU provided route choice decision-making capabilities, based on perception of its environment, that were similar to the described intentions of the driver it represented. The case study clearly demonstrated the feasibility of the approach and the potential to develop more complex driver behavioural dynamics based on the belief-desire-intention agent architecture. (C) 2002 Elsevier Science Ltd. All rights reserved.

Structuring real-time Object-Z specifications

This paper presents a means of structuring specifications in real-time Object-Z: an integration of Object-Z with the timed refinement calculus. Incremental modification of classes using inheritance and composition of classes to form multi-component systems are examined. Two approaches to the latter are considered: using Object-Z's notion of object instantiation and introducing a parallel composition operator similar to those found in process algebras. The parallel composition operator approach is both more concise and allows more general modelling of concurrency. Its incorporation into the existing semantics of real-time Object-Z is presented.

Reproducibility and accuracy of echocardiographic measurements of left ventricular parameters using real-time three-dimensional echocardiography

OBJECTIVES We sought to determine whether assessment of left ventricular (LV) function with real-time (RT) three-dimensional echocardiography (3DE) could reduce the variation of sequential LV measurements and provide greater accuracy than two-dimensional echocardiography (2DE). BACKGROUND Real-time 3DE has become feasible as a standard clinical tool, but its accuracy for LV assessment has not been validated. METHODS Unselected patients (n = 50; 41 men; age, 64 +/- 8 years) presenting for evaluation of LV function were studied with 2DE and RT-3DE. Test-retest variation was performed by a complete restudy by a separate sonographer within 1 h without alteration of hemodynamics or therapy. Magnetic resonance imaging (MRI) images were obtained during a breath-hold, and measurements were made off-line. RESULTS The test-retest variation showed similar measurements for volumes but wider scatter of LV mass measurements with M-mode and 2DE than 3DE. The average MRI end-diastolic volume was 172 +/- 53 ml; LV volumes were underestimated by 2DE (mean difference, -54 +/- 33; p < 0.01) but only slightly by RT-3DE (-4 +/- 29; p = 0.31). Similarly, end-systolic volume by MRI (91 +/- 53 ml) was underestimated by 2DE (mean difference, -28 +/- 28; p < 0.01) and by RT-3DE (mean difference, -3 +/- 18; p = 0.23). Ejection fraction by MRI was similar by 2DE (p = 0.76) and RT-3DE (p = 0.74). Left ventricular mass (183 +/- 50 g) was overestimated by M-mode (mean difference, 68 +/- 86 g; p < 0.01) and 2DE (16 +/- 57; p = 0.04) but not RT-3DE (0 +/- 38 g; p = 0.94). There was good inter- and intra-observer correlation between RT-3DE by two sonographers for volumes, ejection fraction, and mass. CONCLUSIONS Real-time 3DE is a feasible approach to reduce test-retest variation of LV volume, ejection fraction, and mass measurements in follow-up LV assessment in daily practice. (C) 2004 by the American College of Cardiology Foundation.

Detection sensitivity and quantitation of Plasmodium falciparum var gene transcripts by real-time RT-PCR in comparison with conventional RT-PCR

Antigenic variation in Plasmodium falciparum erythrocyte membrane protein 1, caused by a switch in transcription of the encoding var gene, is an important feature of malaria. In this study, we quantified the relative abundance of var gene transcripts present in P. falciparum parasite clones using real-time reverse transcription-polymerase chain reaction (RT-PCR) and conventional RT-PCR combined with cloning and sequencing, with the aim of directly comparing the results obtained. When there was sufficient abundance of RNA for the real-time RT-PCR assay to be operating within the region of good reproducibility, RT-PCR and real-time RT-PCR tended to identify the same dominant transcript, although some transcript-specific issues were identified. When there were differences in the estimated relative amounts of minor transcripts, the RT-PCR assay tended to produce higher estimates than real-time RT-PCR. These results provide valuable information comparing RT-PCR and real-time RT-PCR analysis of samples with small quantities of RNA as might be expected in the analysis of field or clinical samples.