Use of regression equation of peripheral pulse timing characteristics to predict hypertension in children

Studies have shown that an increase in arterial stiffening can indicate the presence of cardiovascular diseases like hypertension. Current gold standard in clinical practice is by measuring the blood pressure of patients using a mercury sphygmomanometer. However, the nature of this technique is not suitable for prolonged monitoring. It has been established that pulse wave velocity is a direct measure of arterial stiffening. However, its usefulness is hampered by the absence of techniques to estimate it non-invasively. Pulse transit time (PTT) is a simple and non-intrusive method derived from pulse wave velocity. It has shown its capability in childhood respiratory sleep studies. Recently, regression equations that can predict PTT values for healthy Caucasian children were formulated. However, its usefulness to identify hypertensive children based on mean PTT values has not been investigated. This was a continual study where 3 more Caucasian male children with known clinical hypertension were recruited. Results indicated that the PTT predictive equations are able to identify hypertensive children from their normal counterparts in a significant manner (p < 0.05). Hence, PTT can be a useful diagnostic tool in identifying hypertension in children and shows potential to be a non-invasive continual monitor for arterial stiffening.

Agent-based distributed software verification

Despite decades of research, the takeup of formal methods for developing provably correct software in industry remains slow. One reason for this is the high cost of proof construction, an activity that, due to the complexity of the required proofs, is typically carried out using interactive theorem provers. In this paper we propose an agent-oriented architecture for interactive theorem proving with the aim of reducing the user interactions (and thus the cost) of constructing software verification proofs. We describe a prototype implementation of our architecture and discuss its application to a small, but non-trivial case study.

A state-of-practice questionnaire on verification and validation for concurrent programs

Research in verification and validation (V&V) for concurrent programs can be guided by practitioner information. A survey was therefore run to gain state-of-practice information in this context. The survey presented in this paper collected state-of-practice information on V&V technology in concurrency from 35 respondents. The results of the survey can help refine existing V&V technology by providing a better understanding of the context of V&V technology usage. Responses to questions regarding the motivation for selecting V&V technologies can help refine a systematic approach to V&V technology selection.

Timing analysis of assembler code control-flow paths

Timinganalysis of assembler code is essential to achieve the strongest possible guarantee of correctness for safety-critical, real-time software. Previous work has shown how timingconstrain ts on controlflow paths through high-level language programs can be formalised using the semantics of the statements comprisingthe path. We extend these results to assembler-level code where it becomes possible to not only determine timingconstrain ts, but also to verify them against the known execution times for each instruction. A minimal formal model is developed with both a weakest liberal precondition and a strongest postcondition semantics. However, despite the formalism’s simplicity, it is shown that complex timingb ehaviour associated with instruction pipeliningand iterative code can be modelled accurately.

Verification and validation of autonomous systems

NASA is working on complex future missions that require cooperation between multiple satellites or rovers. To implement these systems, developers are proposing and using intelligent and autonomous systems. These autonomous missions are new to NASA, and the software development community is just learning to develop such systems. With these new systems, new verification and validation techniques must be used. Current techniques have been developed based on large monolithic systems. These techniques have worked well and reliably, but do not translate to the new autonomous systems that are highly parallel and nondeterministic.