Miracor Eliminates Run-Time Errors and Reduces Testing Time for Class III Medical Device Software

The PiCSO Impulse System has two independent microcontrollers that manage the pressure of the balloon. One serves as the main controller of the pneumatic system, the other as a safety backup. The embedded code for both controllers is written by hand in C.

The engineering team had established code reviews and unit tests to verify this code, but recognized that unit tests alone could not cover all possible combinations of inputs, execution paths, and variable values. They wanted to use control flow– and data flow–based semantic analysis to prove the correctness of software components and detect divide-by-zero, buffer overflow, and other run-time errors.

Miracor needed to comply with the increasingly stringent regulatory requirements for Class III medical devices. The company sought a CE marking in Europe, which requires certification by a notified body as well as premarket approval from the FDA in the U.S. To secure approval from these regulatory agencies, Miracor needed to demonstrate the safety of both hardware and software. Historically, software has presented a larger certification challenge than hardware because it is often more difficult for reviewers to comprehend. Miracor wanted to use static analysis and formal methods to streamline the certification process.

Miracor engineers used Polyspace Code Prover to prove the absence of run-time errors, identify areas of code that needed further review, and increase their overall confidence in the quality of the software.

After participating in a two-day training session provided by MathWorks Training Services, Miracor engineers analyzed their legacy code with Polyspace Code Prover.

Polyspace Code Prover color-coded each C operation to indicate its status: green for code proven free of run-time errors, red for code known to be faulty every time the operation is executed, gray for unreachable (dead) code, and orange for operations that might be faulty under certain conditions.

The team used these results to improve the code. They removed unreachable code, reducing the microcontroller software footprint, and corrected all operations proven faulty, including a divide-by-zero error in a part of the code that was not active in standard operation.

In a subsequent code review, the team focused on the orange highlighted operations, knowing that the remaining green code had been proven to be free of run-time errors.

With multiple embedded microcontrollers operating simultaneously in the PiCSO system, the Miracor team had to be aware of race conditions and other concurrency issues. While configuring Polyspace Code Prover, the team identified several critical areas of code where these conditions could occur.

The team instituted a policy of running Polyspace Code Prover on the project’s roughly 25,000 lines of legacy and newly developed code before each scheduled code review and using the results to help guide each review process.

Miracor’s PiCSO Impulse System has been used to treat patients in the U.K., Ireland, and Hungary. Clinical studies have found statistically significant reductions in infarct size, as well as improvements in cardiac function, following treatment with the system. The company is pursuing premarket approval from the FDA.

• Unused and faulty code identified. “Polyspace Code Prover results showed dead code as well as divide-by-zero and buffer flow errors in our legacy code,” says Christoph Bloch, project manager for software development at Miracor. “Although these errors would not affect patient safety, detecting them gave us greater confidence in the quality of our software.”
• Verification processes for regulatory approval established. “As we seek premarket approval status from the FDA, Polyspace Code Prover is central to our efforts to demonstrate that we have done our utmost to prove code correctness and ensure code quality,” says Schiemanck. “For us, proving that our technology has been verified and validated with Polyspace Code Prover and other state-of-the-art tools is mandatory.”
• Code review efficiency increased. “With Polyspace Code Prover we see what parts of the code are proven safe, so we know where we will not have any run-time errors or arithmetical errors,” says Schiemanck. “As a result, we can review less code because we focus on those parts where potential problems may still exist.”