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
Model checking and static analysis techniques have been successfully applied to some problems, and some of these techniques scale well. However, their analysis targets only certain properties. For critical applications, complete formal verification of functionality is highly desirable.
The Echo approach is intended for routine use alongside existing software development techniques and does not require programmers to be skilled in mathematical logic or formal verification techniques. To ease the burden of creating proofs of correctness, the Echo process splits these into two separate proofs.
A software developer using the Echo process first produces both a formal specification and an annotated SPARK Ada program using familiar, traditional software engineering techniques. Using the SPARK tools, the developer establishes an implementation proof showing that the SPARK Ada source code complies with its annotations. Echo’s unique reverse synthesis process then produces a high-level abstract extracted specification. Finally, the developer establishes an implication proof showing that the extracted specification implies the given formal specification. Taken together, the implementation and implication proofs form a complete proof of correctness.
The keys to the practicality of the Echo process are the use of verification refactoring and the availability of a practical implementation proof process. In verification refactoring, the SPARK program is subjected to user-selected machine transformations. Software must run adequately fast, but this speed often comes at the cost of increased complexity. By transforming the source code into a less complicated form with the same functional semantics, verification refactoring reduces the complexity of the extracted specification. Re-rolling loops, splitting procedures into simpler sub-procedures, reversing function inlining, and adding or removing intermediate computations or storage will not change the program behavior, but can dramatically ease the creation of the required proofs.
The effect of verification refactoring can be dramatic. In one study, Knight and Yin formally verified a SPARK implementation of the Advanced Encryption Standard (AES). By adjusting data structures and reversing table lookups, the efficient implementation to be verified was transformed to one more amenable to formal verification.
While the Echo approach could, in theory, be applied to programs written in any language, SPARK offers a number of advantages, specifically:
- The use of SPARK provides a powerful programming language with associated mechanism for low-level specification.
- SPARK precludes the use of language features that would have made the proofs — both the implementation proof and the implication proof — either extraordinarily difficult or more likely impossible.
- The SPARK tools are robust and mature, and they immediately support the implementation proof that is a fundamental part of the Echo approach.
- Production-quality compilers, such as AdaCore’s GNAT-Pro High-Integrity Edition, are available for many platforms.
The LifeFlow LVAD software project has implemented a control system for the active magnetic bearings that the LVAD uses. A complete verification proof demonstrates that the SPARK implementation refines the high-level PVS specification. The implementation targets a high performance embedded microprocessor. Since no operating system is used, almost all the software that executes has been the subject of formal verification. The only unproven software items are the assembly-language loader, implementations of two low-level C functions called by compiler-generated object code, and the machine configuration parameters.
This article was written by John Knight, PhD, Professor of Computer Science, University of Virginia in Charlottesville, VA; Xiang Yin, Senior Software Design Engineer, MicroStrategy, Inc., Tysons Corner, VA; and Patrick John Graydon, Research Associate, University of York, York, UK.