Miracor Eliminates Run-Time Errors and Reduces Testing Time for Class III Medical Device Software
“From a developer’s perspective, the main advantage of Polyspace Code Prover is a higher level of quality and correctness in the code. Polyspace Code Prover helps Miracor demonstrate this quality and correctness to the regulatory community, including the FDA, to prove that our device is safe.”
Challenge
Ensure the safety of a Class III medical device for improving outcomes for stent recipients
Solution
Use Polyspace Code Prover to prove the absence of run-time errors in the software, guide code reviews, complement functional tests, and support verification processes for regulatory approval
Results
- Unused and faulty code identified
- Verification processes for regulatory approval established
- Code review efficiency increased
Miracor’s PiCSO Impulse System.
Stent implantation can restore coronary blood flow to patients with acute coronary syndrome. However, up to 40% of patients with a stent still have restricted blood flow, which can lead to larger infarcts, poor left ventricular function, and eventual heart failure.
The PiCSO® Impulse System, an innovative therapy developed by Miracor Medical Systems, improves microcirculation and reduces infarct size following stent insertion. The PiCSO (Pressure-Controlled Intermittent Coronary Sinus Occlusion) system inflates a small balloon inserted into the coronary sinus to temporarily block blood outflow, raising coronary venous pressure and forcing blood back into affected tissue. PiCSO control software monitors pressure and synchronizes balloon inflation and deflation with the patient’s electrocardiogram.
As a Class III medical device, the PiCSO system must adhere to the strictest standards for patient safety. To help ensure the safety of its software, Miracor used Polyspace Code Prover™ to detect errors in C code, guide code reviews, and complement functional testing practices.
“Polyspace Code Prover gives us a layer of safety, increases our confidence that our code is free from run-time errors, and enables us to accelerate our code reviews and testing,” says Lars Schiemanck, chief technology officer at Miracor.
Challenge
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.
Solution
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.
Results
- 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.”
Products Used
Related Resources
