我們體檢拍胸片和做 CT 的時候，大家一定都有點擔心輻射的問題。其實我們大可放心，輻射量是嚴格控制在安全范圍內(nèi)的。那么如此復雜的系統(tǒng)，如何做到嚴格控制？

　　醫(yī)療器械在管理上，實行注冊管理制度；開發(fā)上有嚴格的開發(fā)標準，保證了系統(tǒng)的高安全性。軟件開發(fā)方面，要求形式化驗證，保證產(chǎn)品代碼零 BUG。

為什么要零BUG

　　這是一個老問題，也是一個非常重要的問題，還是要在這兒說說。醫(yī)療器械，尤其是第三類醫(yī)療器械，潛在的 BUG 有非常大的風險。如果是在開發(fā)階段，事情還算可控，但是也有修復成本指數(shù)增長的嚴峻問題。

　　如果將問題帶入到產(chǎn)品運營階段，問題就嚴重多了。輕則召回修復，成本急劇上升，重則導致人員傷亡，吃大官司，甚至公司破產(chǎn)。

　　遠的故事，Therac-25案例，造成6起醫(yī)療事故。究其原因，正是因為軟件設(shè)計中沒有考慮計算機可能出現(xiàn)故障，導致原本治療級別的輻射劑量成了100倍劑量的殺人武器。

　　近的故事，F(xiàn)DA公布了保密數(shù)據(jù)庫，570萬起醫(yī)療器械事故首次公之于眾。其中某國際醫(yī)療器械巨頭在2018年秋天報道了一起死亡案例，這起事件與難以編程或校準的胰島素泵軟件有關(guān)。FDA的保密數(shù)據(jù)庫中其他的死亡事件還牽涉兩種心臟起搏器、一種乳房植入物、一種主動脈內(nèi)球囊泵和一臺呼吸機。

Polyspace提供零BUG保障

　　Polyspace主要有2個產(chǎn)品，Polyspace Bug Finder,Polyspace Code Prover，能夠為零BUG保障提供全方面支持。

　　Polyspace Bug Finder用于識別嵌入式軟件C和C++代碼中的運行時錯誤、并發(fā)問題、安全漏洞和其他缺陷；分析軟件控制流、數(shù)據(jù)流和進程間行為；檢查代碼是否符合諸如MISRA-C，JSF++代碼規(guī)范和自定義的命名規(guī)則。

　　Polyspace Code Prover可以證明C和C++源代碼中不存在溢出、被零除、數(shù)組訪問越界以及其他某些運行時錯誤。PolyspaceCodeProver使用靜態(tài)分析和基于形式化方法的抽象解釋法對代碼進行分析，以代碼著色的方式區(qū)分運行時錯誤；計算并顯示變量和函數(shù)返回值的范圍信息，并可以證明變量是否超出指定范圍限制；計算軟件質(zhì)量目標指標并判斷是非達到質(zhì)量目標標準，圖形化形式顯示變量的讀寫及其寫入后的變量范圍。

Polyspace能夠證明代碼無運行時錯誤

　　為了適應(yīng)團隊協(xié)作開發(fā)、自動化驗證，R2019a版本之后，polyspace產(chǎn)品進行了重大升級。升級后的產(chǎn)品包括2個產(chǎn)品組合和6大產(chǎn)品。其中桌面產(chǎn)品包含人機交互界面，用于開發(fā)人員的早期對代碼的驗證，服務(wù)器產(chǎn)品組合用于對項目大量代碼進行自動化驗證構(gòu)建，實現(xiàn)開發(fā)人員、軟件質(zhì)量人員，管理人員的協(xié)同開發(fā)。

　　桌面產(chǎn)品組合
　　Polyspace Bug Finder
　　Polyspace Code Prover

　　服務(wù)器產(chǎn)品組合
　　Polyspace Bug Finder Server
　　Polyspace Bug Finder Access
　　Polyspace Code Prover Server
　　Polyspace Code Prover Access

　　三類醫(yī)療器械和IEC 62304及其與IEC 61508的關(guān)系

　　醫(yī)療器械分為三類，分別為一類，二類和三類。其中第三類是具有高風險，需要采取特別措施嚴格控制管理以保證其安全、有效的醫(yī)療器械。常見的三類醫(yī)療器械主要為一次性使用無菌醫(yī)療器械和人體介入醫(yī)療設(shè)備，如一次性注射器、心臟支架等。這類醫(yī)療器械的出現(xiàn)問題，可能會導致人員嚴重受傷、疾病甚至死亡。

　　IEC 62304是醫(yī)療器械開發(fā)的指導文件，其提供了定義醫(yī)療器械軟件的生命周期要求。標準中描述了軟件開發(fā)的過程、活動和任務(wù)集，為醫(yī)療設(shè)備軟件生命周期過程建立了通用框架。已獲得 FDA 局方的認可。

　　作為IEC 61508的派生標準，IEC 62304并沒有像IEC 61508一樣，在軟件開發(fā)階段，不同等級的軟件不同任務(wù)，推薦技術(shù)、工具和方法，給出推薦。而是直接推薦開發(fā)商直接使用  IEC61508 中的任務(wù)及方法如下圖所示。

　　作為安全等級最高的三類醫(yī)療器械，參考IEC 61508標準的方法。Polyspace能夠提供哪些幫助，完成哪些開發(fā)要求。

Polyspace用于滿足IEC 62304的醫(yī)療器械的開發(fā)

　　Language subset/開發(fā)語言的安全子集

　　表格A.3第3條，針對SIL3/4級別軟件，推薦僅僅使用開發(fā)語言的安全子集，規(guī)避具有安全隱患的語言特性。常見的嵌入式安全子集包括 MISRA C, GJB 5369-2005 等。Polyspace 全面支持包括MISRA C 2004, MISRA C 2012和 MISRA AC AGC。而 GJB 5369-2005 也是依據(jù) MISRA C 藍本編寫，我們可以根據(jù)具體的內(nèi)容建立其間的映射關(guān)系并創(chuàng)建 GJB 5369 檢查項組合。

　　Polyspace針對代碼對規(guī)則的違反，提供一些列快速瀏覽、問題說明和修改建議等，幫助用戶快速解決問題。

Polyspace中MISRAC 2012統(tǒng)計

Polyspace對不符合MISRA C的代碼精確定位，并給出詳細條目、相關(guān)幫助

　　Formal verification/ Formal proof/ Static analysis of run time error behavior（形式化驗證、證明和靜態(tài)分析）

　　附錄表格中多處提到，高等級的軟件需要做形式化驗證，靜態(tài)分析。其中B.8第9條，要求高等級的軟件需要進行靜態(tài)分析，識別出軟件中的運行時錯誤。Polyspace Bug Finder使用靜態(tài)分析的方法，可以識別出軟件可能的運行時錯誤。Bug Finder能夠提供1 大類，258種錯誤，包括關(guān)鍵的數(shù)據(jù)訪問沖突、數(shù)組越界和野指針等嚴重的運行時錯誤。

用戶可以根據(jù)依據(jù)情況定義檢查內(nèi)容

　　表格A.5第10條，明確要求高級別的軟件需要進行形式化驗證，而在表格A.9的第1條，再次要求代碼必須進行形式化證明。可見當前的功能安全規(guī)范已經(jīng)將形式化的方法提高的新的高度。

　　Polyspace Code Prove使用形式化方法對代碼進行分析，告知用戶代碼是否存在運行時錯誤，并以不同顏色標識出來。針對有問題的代碼，使用紅色進行著色，并對問題提供詳細的問題描述，問題發(fā)生的事件圖等。

　　Reverify changed software module/ Reverify affected software modules (軟件變更后的再驗證)

　　在軟件開發(fā)過程中，需求變更是非常常見的。如果在項目的中后期，代碼的更改必須進行全面的分析并做回歸測試。表格 A.8 的第 2 條和第 3 條就是這方面的要求。為了徹底的分析代碼變更的影響，功能安全軟件的全面的分析很有必要。Polyspace Code Prover access 和  Polyspace Code Prover Server 能夠與常見的自動化工具如  Jenkins 集成，當回歸測試的代碼進入代碼庫后，Jenkins會自動構(gòu)建新的分析，并將分析結(jié)果保存到 access 中，團隊其他成員可以查看結(jié)果。如技術(shù)經(jīng)理監(jiān)控當前的軟件質(zhì)量目標。如果因為代碼變更引入的新的問題，質(zhì)量保證人員根據(jù)分析結(jié)果，分配 JIRA 問題單給相關(guān)責任人。

　　Limited use of pointers / Limited use of recursion（限制指針和遞歸使用）

　　規(guī)范在附錄表格 B.1 第 5 條和第 6 條分別限制了在功能安全軟件中對指針和遞歸的使用，對于 SIL3/4 級的軟件，必須遵守的規(guī)定，限制因為語言復雜引發(fā)的軟件行為不確定性。MISRA C 中的部分條款已經(jīng)對指針的限制使用做了規(guī)定。其他方面，polyspace code prover 為提供指針非法引用的檢查，并提供詳細的證明信息。

　　在遞歸方面，Polyspace Bug Finder 提供代碼度量，包括代碼的圈復雜度、遞歸度等，并生成報告作為產(chǎn)品驗證的證物。

　　Boundary value analysis (邊界值分析)

　　做過開發(fā)的同學都知道，大量的錯誤是發(fā)生在輸入判定的邊界或輸出范圍的邊界上，尤其是變量超出該類型的邊界，引發(fā)運行時錯誤，導致安全事故。雖然針對各種邊界情況設(shè)計測試用例，可以查出更多的軟件錯誤。但是始終不能做到對所有邊界值進行全方面掌握。

　　Polyspace Code Prover 在對代碼進行分析的同時，會對代碼中的所有變量進行范圍分析，并給出變量在某個代碼行處的取值范圍，讓變量的所有可能取值一目了然。

　　Control flow analysis （控制流分析）

　　一方面，Polyspace Code Prover 在進行代碼分析時，灰色的代碼表示代碼不可達，表明代碼的控制流存在問題。另一方面，Polyspace Code Prover 能夠提取驗證 C 代碼中的控制流信息并生成調(diào)用樹，讓用戶能夠一目了然了解到當前軟件的控制流情況。Polyspace Code Prover 能夠為系統(tǒng)函數(shù)調(diào)用關(guān)系生成報告。

調(diào)用結(jié)構(gòu)報告

　　Data flow analysis（數(shù)據(jù)流分析）

　　Polyspace Code Prover 依據(jù)抽象演繹法對代碼進行代碼靜態(tài)分析，在分析中，包含對代碼的動態(tài)屬性進行驗證，也就是針對代碼中的每個變量的在代碼中的數(shù)據(jù)流確定其動態(tài)屬性，Code Prover 依據(jù)數(shù)據(jù)流，對代碼進行演繹分析，并能夠?qū)?shù)據(jù)的訪問情況以樹狀結(jié)構(gòu)表示出來。

Polyspace Code Prover 提供的變量訪問數(shù)

　　Polyspace通過TüV SüD認證

　　使用 IEC Certification Kit，幫助用戶快速通過 Polyspace 認證。IEC Certification Kit 提供了工具認證工件、證書和測試套件，并生成可跟蹤性矩陣。該工具包幫助您驗證 Polyspace，并簡化嵌入式系統(tǒng)到 IEC 62304 的認證中。

Polyspace 的 TüV SüD 認證

認證報告指出，形式化工具Polyspace的使用，可以降低測試覆蓋度要求。

總結(jié)

　　醫(yī)療器械的功能安全一直是生產(chǎn)商至始至終繞不開的話題，也是生產(chǎn)商最基本的企業(yè)責任之一。但是這個企業(yè)責任確實不好做，尤其是，隨著醫(yī)療器械的電氣化程度越來越高，軟件復雜度指數(shù)級增加。那么企業(yè)如何面對這些嚴峻的問題? Polyspace 給出了這樣一份答卷。它能夠幫助您查找軟件中的缺陷，證明您的軟件系統(tǒng)沒有運行時錯誤，并且支持您將它作為 IEC 62304 認證的工具，獲得 FDA/CE 的認證。