miracle消除了III类医疗设备软件的运行时错误并减少了测试时间

PiCSO脉冲系统有两个独立的微控制器来控制气球的压力。一个作为气动系统的主控制器，另一个作为安全备份。两个控制器的嵌入式代码都是用C语言手工编写的。

工程团队已经建立了代码评审和单元测试来验证此代码，但是认识到单元测试本身并不能覆盖所有可能的输入、执行路径和变量值的组合。他们希望使用基于控制流和数据流的语义分析来证明软件组件的正确性，并检测除零、缓冲区溢出和其他运行时错误。

Miracor需要遵守对III类医疗器械日益严格的监管要求。该公司在欧洲寻求CE标志，这需要通知机构的认证以及美国FDA的上市前批准。为了获得这些监管机构的批准，Miracor需要证明硬件和软件的安全性。从历史上看，软件比硬件带来了更大的认证挑战，因为审查人员往往更难理解。Miracor希望使用静态分析和形式化方法来简化认证过程。

Miracor的工程师使用Polyspace Code Prover来证明没有运行时错误，识别需要进一步检查的代码区域，并增加他们对软件质量的总体信心。

在参加了MathWorks培训服务提供的为期两天的培训课程后，Miracor工程师使用Polyspace code Prover分析了他们的遗留代码。

Polyspace Code Prover用颜色对每个C操作进行编码，以指示其状态:绿色表示已证实无运行时错误的代码，红色表示每次执行操作时已知有错误的代码，灰色表示不可访问(失效)代码，橙色表示在某些条件下可能有错误的操作。

团队使用这些结果来改进代码。他们删除了无法访问的代码，减少了微控制器软件占用空间，并纠正了所有被证明有故障的操作，包括标准操作中未激活的代码部分中的除零错误。

在随后的代码评审中，团队将重点放在橙色突出显示的操作上，知道剩余的绿色代码已经被证明没有运行时错误。

由于PiCSO系统中同时运行多个嵌入式微控制器，Miracor团队必须了解竞争条件和其他并发问题。在配置Polyspace代码验证程序时，团队确定了可能出现这些情况的几个关键代码区域。

团队制定了一项政策，在每次计划的代码评审之前，在项目的大约25000行遗留代码和新开发的代码上运行Polyspace代码验证程序，并使用结果帮助指导每次评审过程。

MIRACOR的PICSO脉冲系统已被用于治疗英国、爱尔兰和匈牙利的患者。临床研究发现，使用该系统治疗后，梗死面积在统计学上显著减少，心功能也得到改善。该公司正在寻求FDA的上市前批准。

• 识别出未使用和故障代码。Miracor软件开发项目经理Christoph Bloch说:“Polyspace Code Prover的结果显示，遗留代码中存在死代码、除以零和缓冲区流错误。”“尽管这些错误不会影响患者的安全，但发现它们让我们对我们的软件质量有了更大的信心。”
• 建立了监管批准的验证流程。Schiemanck说：“在我们寻求FDA的上市前批准状态时，Polyspace代码验证程序是我们努力证明我们已尽最大努力证明代码正确性并确保代码质量的核心。”。“对我们来说，必须证明我们的技术已通过Polyspace Code Prover和其他最先进的工具进行了验证和验证。”
• 代码检查效率提高。Schiemanck说:“通过Polyspace Code Prover，我们可以看到代码的哪些部分被证明是安全的，因此我们知道哪里不会出现运行时错误或算术错误。“因此，我们可以审查更少的代码，因为我们关注的是那些潜在问题可能仍然存在的部分。”