INTRODUCING: The LifeFlow Left Ventricular Assist Device

Healthcare Global talks to Professor John Knight about a prototype artificial heart pump designed for the long-term treatment of heart failure. John talks about how this life-changing technology has been developed and how software reliability is achieved using ‘SPARK’, AdaCore’s toolkit for the Ada programming language. John envisions a medical future where computers will increasingly play a role in safeguarding the lives of patients in our hospitals.

HCG: What is the LifeFlow Left Ventricular Assist Device (LVAD) and how does it work?

JK: An LVAD is a device that supplements the pumping capability of the left ventricle for patients with insufficient natural pumping capacity. Heart failure occurs when the heart loses its ability to pump enough blood through the body. With the LifeFlow, a patient’s heart pumping can be supplemented synthetically. Magnetic bearings suspend a rotating entity such as the impeller in the LifeFlow in a magnetic field, thereby eliminating the need for mechanical support. These bearings allow a pump to be built without mechanical contact between the impeller and the casing. This helps to reduce damage to blood cells.

What are the benefits of the device to patients?

There are many benefits, but an important one is the prospect for reducing blood-cell damage.

How is reliability maintained so that patients can trust the technology and be sure that their wellbeing is being safeguarded?

The software in medical devices has a very high cost of failure (the patient might be injured), and so ultra-high levels of dependability are required. In complex devices such as the LifeFlow, some of the computations have to be carried out in real time. Assurance is best obtained by appealing to formal (mathematical) languages and mathematical proofs. The statement of what the software has to do in the LifeFlow, called the specification, was prepared in a mathematical language and many of the properties of the software were checked using an automatic theorem prover.

Tell me more about the 'Echo process' and how doctors can put their trust in software written by computers.

Echo is a new software technology developed at the University of Virginia. The proof for LifeFlow was actually created by computers, not humans, and the entire Echo approach relies heavily on the existing capabilities of SPARK Ada and its associated tools. 

Are there any plans for the 'LifeFlow' prototype to be implemented in hospitals?

The current state of the project is that it remains at the early prototype stage and is ‘on hold’ because no manufacturer has been identified who can fabricate the intricate form of the impeller and casing.

Do you envisage similar devices being key players in the future of healthcare technology?

Devices that include powerful computers and innovative software seem very likely to contribute to the future of healthcare technology. As can be seen in the current generation of devices, computers bring new opportunities for functionality for healthcare systems.

What technology do you think will lead the way in terms of healthcare innovation in the next decade?

The future of healthcare innovation will certainly include software-intensive digital systems. Technology that provides the necessary software productivity and dependability will very likely be a major player in healthcare innovation.

John Knight is a professor of computer science at the University of Virginia. He holds a B.Sc. (Hons) in Mathematics from the Imperial College of Science and Technology (London) and a Ph.D. in Computer Science from the University of Newcastle upon Tyne. Prior to joining the University of Virginia in 1981, he was with NASA's Langley Research Centre.