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

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

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

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

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

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

Polyspace Code Prover用颜色对每个C操作进行编码，以指示其状态:绿色表示被证明没有运行时错误的代码，红色表示每次执行操作时已知的错误代码，灰色表示不可访问(死)代码，橙色表示在特定条件下可能发生错误的操作。

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

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

由于PiCSO系统中有多个嵌入式微控制器同时工作，Miracor团队必须意识到竞态条件和其他并发性问题。在配置Polyspace代码验证器时，团队确定了几个可能发生这些情况的关键代码区域。

团队制定了一个策略，在每次预定的代码评审之前，在项目的大约25000行遗留代码和新开发的代码上运行Polyspace Code Prover，并使用结果来帮助指导每次评审过程。

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

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