Ensure the safety of a Class III medical device for improving outcomes for stent recipients
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
“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.”Lars Schiemanck, Miracor Medical Systems
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.
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.