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

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

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

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

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

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

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

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

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

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

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

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

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