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

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

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

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

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

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

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

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

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

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

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

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

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