University of Virginia (USA)
ECHO: A Practical Approach to Formal Verification
At the University of Virginia, Ada lies at the core of a comprehensive approach to creating software for safety-critical applications. Dr. John Knight and his student, Xiang Yin, have created a practical approach to formal verification called Echo. In Echo verification, a program written in SPARK Ada is verified to conform to its SPARK annotations using the SPARK tools.
Echo’s strategy of splitting the formal verification process down the middle and attacking it from both sides dramatically reduces the effort needed to complete a formal verification, enabling Dr. Knight and his students to complete verification of systems as large as 10,000 lines of Ada code.
One project that has benefited from Ada and Echo verification is the University of Virginia’s LifeFlow artificial heart pump. Designed for the long-term (10–20 year) treatment of heart failure, this pump has a continuous-flow, axial design. The use of magnetic bearings and computational fluid dynamics simulations permit a streamlined path for blood flow. Compared with earlier pumps that used mechanical bearings, this flow path reduces the damage done to blood cells, thus reducing the potential for the formation of dangerous blood clots.
Control of the magnetic bearings is provided by a Freescale MPC5554 microcontroller executing control software written in SPARK Ada by Patrick Graydon and compiled using AdaCore’s GNAT Pro High-Integrity Edition compiler. The control software runs natively on the microcontroller with no operating system, limiting the software base that must be verified for this safety-critical application. Comprehensive Echo formal verification complements functional testing to Modified Condition / Decision Coverage (MC/DC), providing high confidence that the magnetic bearing controller is as free of defects as can practically be achieved.
Formally Verifying Heart Pump Software with SPARK and Echo »