我們體檢拍胸片和做 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 的認證。