The Ada-based SPARK programming language and toolset offer strong guarantees about the behavior of software systems. This powerful core underpins Echo, a complete approach to practical formal verification developed at the University of Virginia, Charlottesville, by Dr. John Knight and his student, Xiang Yin. Echo extends the verification power afforded by the SPARK tools and the PVS Specification and Verification System to provide a complete proof that a given SPARK implementation re fines its formal specification.
The UVA LifeFlow LVAD
The University of Virginia LifeFlow Left Ventricular Assist Device (LVAD) is a prototype artificial heart pump designed for the long-term (10–20 year) treatment of heart failure. LifeFlow has a continuous- flow, axial design. (See Figure 1) Magnetic bearings and a brushless DC motor keep the pump’s impeller centered in the pump housing and turning without the need for mechanical bearings or shaft seals. The elimination of pinch points, coupled with careful design of the pump cavity, impeller, and blades, and aided by computational fluid dynamics simulations, minimizes damage to blood cells and reduces the potential for forming clots.
A digital control algorithm running on a Freescale MPC 5554 microcontroller provides control of the magnetic suspension bearings. The impeller, which turns at 8,000 RPM within 0.1 mm of the pump cavity walls, must be kept centered despite the forces imparted by gravity, blood flow and surge, and the patient’s movement. In hard real time, the controller must sample the position of the rotor as reported by a self-sensing circuit, compute the coil currents necessary to keep the rotor adequately centered, and direct the coil driver to achieve those currents. Both individual magnetic coils and the wires connecting them to the control circuits can fail. The control software is required to be capable of reconfiguring to a variety of backup modes in which rotor levitation is accomplished with only two of three coil pairs.
Since a failure of the magnetic bearings could cause a failure of the pump and possible injury to the patient, the magnetic bearing control software must be as free of defects as is reasonably practical. Dr. Patrick Graydon developed software for the prototype using Altran Praxis’ SPARK toolset and AdaCore’s GNAT Pro High-Integrity Edition Ada compiler. To achieve the necessary assurance, Yin and Graydon subjected the implementation to a complete formal verification using the Echo process. (See Figure 2)
The SPARK Programming Language and Tools
SPARK is a high-level, high-integrity software development language supported by powerful tools. Designed by Altran Praxis (previously Praxis High Integrity Systems), SPARK is an Ada subset augmented by a notation for specifying a program’s “contracts.” Contracts, also known as annotations, are expressed through a structured Ada comment syntax and support a style of program development known as Correctness by Construction.
One element of a program's contract, in both Ada and SPARK, is a subprogram’s “signature” — its name, parameters (including their types and modes), and result type (if a function). SPARK programs have additional contractual elements: a set of core annotations, possibly supplemented by more specific proof annotations. The core annotations allow a fast (polynomial-time) analysis of SPARK source code to check for data-flow and information-flow errors. Such errors (for example, an attempt to read the value of an uninitialized variable) can indicate a failure of the code to meet its contract.
The Ada subset at the heart of the SPARK language has been chosen to produce a simple yet powerful programming language, retaining the key features that support the construction of software that is demonstrably correct. Because the restricted language subset excludes features that complicate static analysis, the tools are able to prove many of the requisite properties automatically.
Practical Formal Verification Using Echo
The Echo process is a practical approach to formal verification that builds upon the capabilities of the SPARK toolset. Testing alone is not a feasible means to achieve the necessary levels of assurance for critical applications. To supplement testing, developers might choose one of three forms of formal verification: correctness proofs, refinement, and model checking and static analysis.
Proving that a given source program correctly implements a given formal specification can be very challenging, even with machine assistance. Both the cumulative detail for the program and the complexity of individual predicates associated with elaborate or intricate source statements can easily overwhelm available machine resources.
Refinement approaches have been created to address these difficulties. In refinement approaches, a formal specification is repeatedly refined through a series of transformations. However, two important limitations make the refinement approach impractical or undesirable for many applications:
- Many existing software development techniques cannot be used because software development is constrained by the simultaneous proof development
- New or updated requirements necessitate revisiting every intermediate artifact in the refinement path