我们体检拍胸片和做 CT 的时候，大家一定都有点担心辐射的问题。其实我们大可放心，辐射量是严格控制在安全范围内的。那么如此复杂的系统，如何做到严格控制？

　　医疗器械在管理上，实行注册管理制度；开发上有严格的开发标准，保证了系统的高安全性。软件开发方面，要求形式化验证，保证产品代码零 BUG。

为什么要零BUG

　　这是一个老问题，也是一个非常重要的问题，还是要在这儿说说。医疗器械，尤其是第三类医疗器械，潜在的 BUG 有非常大的风险。如果是在开发阶段，事情还算可控，但是也有修复成本指数增长的严峻问题。

　　如果将问题带入到产品运营阶段，问题就严重多了。轻则召回修复，成本急剧上升，重则导致人员伤亡，吃大官司，甚至公司破产。

　　远的故事，Therac-25案例，造成6起医疗事故。究其原因，正是因为软件设计中没有考虑计算机可能出现故障，导致原本治疗级别的辐射剂量成了100倍剂量的杀人武器。

　　近的故事，FDA公布了保密数据库，570万起医疗器械事故首次公之于众。其中某国际医疗器械巨头在2018年秋天报道了一起死亡案例，这起事件与难以编程或校准的胰岛素泵软件有关。FDA的保密数据库中其他的死亡事件还牵涉两种心脏起搏器、一种乳房植入物、一种主动脉内球囊泵和一台呼吸机。

Polyspace提供零BUG保障

　　Polyspace主要有2个产品，Polyspace Bug Finder,Polyspace Code Prover，能够为零BUG保障提供全方面支持。

　　Polyspace Bug Finder用于识别嵌入式软件C和C++代码中的运行时错误、并发问题、安全漏洞和其他缺陷；分析软件控制流、数据流和进程间行为；检查代码是否符合诸如MISRA-C，JSF++代码规范和自定义的命名规则。

　　Polyspace Code Prover可以证明C和C++源代码中不存在溢出、被零除、数组访问越界以及其他某些运行时错误。PolyspaceCodeProver使用静态分析和基于形式化方法的抽象解释法对代码进行分析，以代码着色的方式区分运行时错误；计算并显示变量和函数返回值的范围信息，并可以证明变量是否超出指定范围限制；计算软件质量目标指标并判断是非达到质量目标标准，图形化形式显示变量的读写及其写入后的变量范围。

Polyspace能够证明代码无运行时错误

　　为了适应团队协作开发、自动化验证，R2019a版本之后，polyspace产品进行了重大升级。升级后的产品包括2个产品组合和6大产品。其中桌面产品包含人机交互界面，用于开发人员的早期对代码的验证，服务器产品组合用于对项目大量代码进行自动化验证构建，实现开发人员、软件质量人员，管理人员的协同开发。

　　桌面产品组合
　　Polyspace Bug Finder
　　Polyspace Code Prover

　　服务器产品组合
　　Polyspace Bug Finder Server
　　Polyspace Bug Finder Access
　　Polyspace Code Prover Server
　　Polyspace Code Prover Access

　　三类医疗器械和IEC 62304及其与IEC 61508的关系

　　医疗器械分为三类，分别为一类，二类和三类。其中第三类是具有高风险，需要采取特别措施严格控制管理以保证其安全、有效的医疗器械。常见的三类医疗器械主要为一次性使用无菌医疗器械和人体介入医疗设备，如一次性注射器、心脏支架等。这类医疗器械的出现问题，可能会导致人员严重受伤、疾病甚至死亡。

　　IEC 62304是医疗器械开发的指导文件，其提供了定义医疗器械软件的生命周期要求。标准中描述了软件开发的过程、活动和任务集，为医疗设备软件生命周期过程建立了通用框架。已获得 FDA 局方的认可。

　　作为IEC 61508的派生标准，IEC 62304并没有像IEC 61508一样，在软件开发阶段，不同等级的软件不同任务，推荐技术、工具和方法，给出推荐。而是直接推荐开发商直接使用  IEC61508 中的任务及方法如下图所示。

　　作为安全等级最高的三类医疗器械，参考IEC 61508标准的方法。Polyspace能够提供哪些帮助，完成哪些开发要求。

Polyspace用于满足IEC 62304的医疗器械的开发

　　Language subset/开发语言的安全子集

　　表格A.3第3条，针对SIL3/4级别软件，推荐仅仅使用开发语言的安全子集，规避具有安全隐患的语言特性。常见的嵌入式安全子集包括 MISRA C, GJB 5369-2005 等。Polyspace 全面支持包括MISRA C 2004, MISRA C 2012和 MISRA AC AGC。而 GJB 5369-2005 也是依据 MISRA C 蓝本编写，我们可以根据具体的内容建立其间的映射关系并创建 GJB 5369 检查项组合。

　　Polyspace针对代码对规则的违反，提供一些列快速浏览、问题说明和修改建议等，帮助用户快速解决问题。

Polyspace中MISRAC 2012统计

Polyspace对不符合MISRA C的代码精确定位，并给出详细条目、相关帮助

　　Formal verification/ Formal proof/ Static analysis of run time error behavior（形式化验证、证明和静态分析）

　　附录表格中多处提到，高等级的软件需要做形式化验证，静态分析。其中B.8第9条，要求高等级的软件需要进行静态分析，识别出软件中的运行时错误。Polyspace Bug Finder使用静态分析的方法，可以识别出软件可能的运行时错误。Bug Finder能够提供1 大类，258种错误，包括关键的数据访问冲突、数组越界和野指针等严重的运行时错误。

用户可以根据依据情况定义检查内容

　　表格A.5第10条，明确要求高级别的软件需要进行形式化验证，而在表格A.9的第1条，再次要求代码必须进行形式化证明。可见当前的功能安全规范已经将形式化的方法提高的新的高度。

　　Polyspace Code Prove使用形式化方法对代码进行分析，告知用户代码是否存在运行时错误，并以不同颜色标识出来。针对有问题的代码，使用红色进行着色，并对问题提供详细的问题描述，问题发生的事件图等。

　　Reverify changed software module/ Reverify affected software modules (软件变更后的再验证)

　　在软件开发过程中，需求变更是非常常见的。如果在项目的中后期，代码的更改必须进行全面的分析并做回归测试。表格 A.8 的第 2 条和第 3 条就是这方面的要求。为了彻底的分析代码变更的影响，功能安全软件的全面的分析很有必要。Polyspace Code Prover access 和  Polyspace Code Prover Server 能够与常见的自动化工具如  Jenkins 集成，当回归测试的代码进入代码库后，Jenkins会自动构建新的分析，并将分析结果保存到 access 中，团队其他成员可以查看结果。如技术经理监控当前的软件质量目标。如果因为代码变更引入的新的问题，质量保证人员根据分析结果，分配 JIRA 问题单给相关责任人。

　　Limited use of pointers / Limited use of recursion（限制指针和递归使用）

　　规范在附录表格 B.1 第 5 条和第 6 条分别限制了在功能安全软件中对指针和递归的使用，对于 SIL3/4 级的软件，必须遵守的规定，限制因为语言复杂引发的软件行为不确定性。MISRA C 中的部分条款已经对指针的限制使用做了规定。其他方面，polyspace code prover 为提供指针非法引用的检查，并提供详细的证明信息。

　　在递归方面，Polyspace Bug Finder 提供代码度量，包括代码的圈复杂度、递归度等，并生成报告作为产品验证的证物。

　　Boundary value analysis (边界值分析)

　　做过开发的同学都知道，大量的错误是发生在输入判定的边界或输出范围的边界上，尤其是变量超出该类型的边界，引发运行时错误，导致安全事故。虽然针对各种边界情况设计测试用例，可以查出更多的软件错误。但是始终不能做到对所有边界值进行全方面掌握。

　　Polyspace Code Prover 在对代码进行分析的同时，会对代码中的所有变量进行范围分析，并给出变量在某个代码行处的取值范围，让变量的所有可能取值一目了然。

　　Control flow analysis （控制流分析）

　　一方面，Polyspace Code Prover 在进行代码分析时，灰色的代码表示代码不可达，表明代码的控制流存在问题。另一方面，Polyspace Code Prover 能够提取验证 C 代码中的控制流信息并生成调用树，让用户能够一目了然了解到当前软件的控制流情况。Polyspace Code Prover 能够为系统函数调用关系生成报告。

调用结构报告

　　Data flow analysis（数据流分析）

　　Polyspace Code Prover 依据抽象演绎法对代码进行代码静态分析，在分析中，包含对代码的动态属性进行验证，也就是针对代码中的每个变量的在代码中的数据流确定其动态属性，Code Prover 依据数据流，对代码进行演绎分析，并能够将数据的访问情况以树状结构表示出来。

Polyspace Code Prover 提供的变量访问数

　　Polyspace通过TüV SüD认证

　　使用 IEC Certification Kit，帮助用户快速通过 Polyspace 认证。IEC Certification Kit 提供了工具认证工件、证书和测试套件，并生成可跟踪性矩阵。该工具包帮助您验证 Polyspace，并简化嵌入式系统到 IEC 62304 的认证中。

Polyspace 的 TüV SüD 认证

认证报告指出，形式化工具Polyspace的使用，可以降低测试覆盖度要求。

总结

　　医疗器械的功能安全一直是生产商至始至终绕不开的话题，也是生产商最基本的企业责任之一。但是这个企业责任确实不好做，尤其是，随着医疗器械的电气化程度越来越高，软件复杂度指数级增加。那么企业如何面对这些严峻的问题? Polyspace 给出了这样一份答卷。它能够帮助您查找软件中的缺陷，证明您的软件系统没有运行时错误，并且支持您将它作为 IEC 62304 认证的工具，获得 FDA/CE 的认证。