Can myocardial contrast echo provide incremental benefit to exercise echo? Implications of the intensity and duration of hyperaemia

Background. Stress myocardial contrast echo (MCE) is technically challenging with exercise (Ex) because of cardiacmovementandshort duration ofhyperemia.Vasodilators solve these limitations, but are less potent for inducing abnormal wall motion (WM). We sought whether a combined dipyridamole (DI; 0.56 mg/kg i.v. 4 min) and Ex stress protocol would enable MCE to provide incremental benefit toWManalysis for detection of CAD. Methods. Standard echo images were followed by real time MCE at rest and following stress in 85 pts, 70 undergoing quantitative coronary angiography and 15 low risk pts.WMAfrom standard and LVopacification images, and then myocardial perfusion were assessed sequentially in a blinded fashion. A subgroup of 13 pts also underwent Ex alone, to assess the contribution of DI to quantitative myocardial flow reserve (MFR). Results. Significant (>50%) stenoses were present in 43 pts, involving 69 territories. Addition of MCE improved SE sensitivity for detection of CAD (91% versus 74%, P = 0.02) and better appreciation of disease extent (87% versus 65%territories, P=0.003), with a non-significant reduction in specificity. In 55 territories subtended by a significant stenosis, but with no resting WM abnormality, ability to identify ischemia was also significantly increased by MCE (82% versus 60%, P = 0.002). MFR was less with Ex alone than with DIEx stress (2.4 ± 1.6 versus 4.0 ± 1.9, P = 0.05), suggesting prolongation of hyperaemia with DI may be essential to the results. Conclusions. Dipyridamole-exercise MCE adds significant incremental benefit to standard SE, with improved diagnostic sensitivity and more accurate estimation of extent of CAD.

Axiomatisation of an Interval Calculus for Theorem Proving

We provide an axiomatisation of the Timed Interval Calculus, a set-theoretic notation for expressing properties of time intervals. We implement the axiomatisation in the Ergo theorem prover in order to allow the machine-checked proof of laws for reasoning about predicates expressed using interval operators. These laws can be then used in the machine-assisted verification of real-time applications.

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.

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.