我們體檢拍胸片和做 CT 的時(shí)候，大家一定都有點(diǎn)擔(dān)心輻射的問(wèn)題。其實(shí)我們大可放心，輻射量是嚴(yán)格控制在安全范圍內(nèi)的。那么如此復(fù)雜的系統(tǒng)，如何做到嚴(yán)格控制？
醫(yī)療器械在管理上，實(shí)行注冊(cè)管理制度；開(kāi)發(fā)上有嚴(yán)格的開(kāi)發(fā)標(biāo)準(zhǔn)，保證了系統(tǒng)的高安全性。軟件開(kāi)發(fā)方面，要求形式化驗(yàn)證，保證產(chǎn)品代碼零 BUG。
為什么要零BUG
這是一個(gè)老問(wèn)題，也是一個(gè)非常重要的問(wèn)題，還是要在這兒說(shuō)說(shuō)。醫(yī)療器械，尤其是第三類醫(yī)療器械，潛在的 BUG 有非常大的風(fēng)險(xiǎn)。如果是在開(kāi)發(fā)階段，事情還算可控，但是也有修復(fù)成本指數(shù)增長(zhǎng)的嚴(yán)峻問(wèn)題。
如果將問(wèn)題帶入到產(chǎn)品運(yùn)營(yíng)階段，問(wèn)題就嚴(yán)重多了。輕則召回修復(fù)，成本急劇上升，重則導(dǎo)致人員傷亡，吃大官司，甚至公司破產(chǎn)。
遠(yuǎn)的故事，Therac-25案例，造成6起醫(yī)療事故。究其原因，正是因?yàn)檐浖O(shè)計(jì)中沒(méi)有考慮計(jì)算機(jī)可能出現(xiàn)故障，導(dǎo)致原本治療級(jí)別的輻射劑量成了100倍劑量的殺人武器。
近的故事，F(xiàn)DA公布了保密數(shù)據(jù)庫(kù)，570萬(wàn)起醫(yī)療器械事故首次公之于眾。其中某國(guó)際醫(yī)療器械巨頭在2018年秋天報(bào)道了一起死亡案例，這起事件與難以編程或校準(zhǔn)的胰島素泵軟件有關(guān)。FDA的保密數(shù)據(jù)庫(kù)中其他的死亡事件還牽涉兩種心臟起搏器、一種乳房植入物、一種主動(dòng)脈內(nèi)球囊泵和一臺(tái)呼吸機(jī)。
Polyspace提供零BUG保障
Polyspace主要有2個(gè)產(chǎn)品，Polyspace Bug Finder,Polyspace Code Prover，能夠?yàn)榱鉈UG保障提供全方面支持。
Polyspace Bug Finder用于識(shí)別嵌入式軟件C和C++代碼中的運(yùn)行時(shí)錯(cuò)誤、并發(fā)問(wèn)題、安全漏洞和其他缺陷；分析軟件控制流、數(shù)據(jù)流和進(jìn)程間行為；檢查代碼是否符合諸如MISRA-C，JSF++代碼規(guī)范和自定義的命名規(guī)則。
Polyspace Code Prover可以證明C和C++源代碼中不存在溢出、被零除、數(shù)組訪問(wèn)越界以及其他某些運(yùn)行時(shí)錯(cuò)誤。PolyspaceCodeProver使用靜態(tài)分析和基于形式化方法的抽象解釋法對(duì)代碼進(jìn)行分析，以代碼著色的方式區(qū)分運(yùn)行時(shí)錯(cuò)誤；計(jì)算并顯示變量和函數(shù)返回值的范圍信息，并可以證明變量是否超出指定范圍限制；計(jì)算軟件質(zhì)量目標(biāo)指標(biāo)并判斷是非達(dá)到質(zhì)量目標(biāo)標(biāo)準(zhǔn)，圖形化形式顯示變量的讀寫(xiě)及其寫(xiě)入后的變量范圍。
Polyspace能夠證明代碼無(wú)運(yùn)行時(shí)錯(cuò)誤
為了適應(yīng)團(tuán)隊(duì)協(xié)作開(kāi)發(fā)、自動(dòng)化驗(yàn)證，R2019a版本之后，polyspace產(chǎn)品進(jìn)行了重大升級(jí)。升級(jí)后的產(chǎn)品包括2個(gè)產(chǎn)品組合和6大產(chǎn)品。其中桌面產(chǎn)品包含人機(jī)交互界面，用于開(kāi)發(fā)人員的早期對(duì)代碼的驗(yàn)證，服務(wù)器產(chǎn)品組合用于對(duì)項(xiàng)目大量代碼進(jìn)行自動(dòng)化驗(yàn)證構(gòu)建，實(shí)現(xiàn)開(kāi)發(fā)人員、軟件質(zhì)量人員，管理人員的協(xié)同開(kāi)發(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ī)療器械分為三類，分別為一類，二類和三類。其中第三類是具有高風(fēng)險(xiǎn)，需要采取特別措施嚴(yán)格控制管理以保證其安全、有效的醫(yī)療器械。常見(jiàn)的三類醫(yī)療器械主要為一次性使用無(wú)菌醫(yī)療器械和人體介入醫(yī)療設(shè)備，如一次性注射器、心臟支架等。這類醫(yī)療器械的出現(xiàn)問(wèn)題，可能會(huì)導(dǎo)致人員嚴(yán)重受傷、疾病甚至死亡。
IEC 62304是醫(yī)療器械開(kāi)發(fā)的指導(dǎo)文件，其提供了定義醫(yī)療器械軟件的生命周期要求。標(biāo)準(zhǔn)中描述了軟件開(kāi)發(fā)的過(guò)程、活動(dòng)和任務(wù)集，為醫(yī)療設(shè)備軟件生命周期過(guò)程建立了通用框架。已獲得 FDA 局方的認(rèn)可。
作為IEC 61508的派生標(biāo)準(zhǔn)，IEC 62304并沒(méi)有像IEC 61508一樣，在軟件開(kāi)發(fā)階段，不同等級(jí)的軟件不同任務(wù)，推薦技術(shù)、工具和方法，給出推薦。而是直接推薦開(kāi)發(fā)商直接使用 IEC61508 中的任務(wù)及方法如下圖所示。
作為安全等級(jí)最高的三類醫(yī)療器械，參考IEC 61508標(biāo)準(zhǔn)的方法。Polyspace能夠提供哪些幫助，完成哪些開(kāi)發(fā)要求。
Polyspace用于滿足IEC 62304的醫(yī)療器械的開(kāi)發(fā)
Language subset/開(kāi)發(fā)語(yǔ)言的安全子集
表格A.3第3條，針對(duì)SIL3/4級(jí)別軟件，推薦僅僅使用開(kāi)發(fā)語(yǔ)言的安全子集，規(guī)避具有安全隱患的語(yǔ)言特性。常見(jiàn)的嵌入式安全子集包括 MISRA C, GJB 5369-2005 等。Polyspace 全面支持包括MISRA C 2004, MISRA C 2012和 MISRA AC AGC。而 GJB 5369-2005 也是依據(jù) MISRA C 藍(lán)本編寫(xiě)，我們可以根據(jù)具體的內(nèi)容建立其間的映射關(guān)系并創(chuàng)建 GJB 5369 檢查項(xiàng)組合。
Polyspace針對(duì)代碼對(duì)規(guī)則的違反，提供一些列快速瀏覽、問(wèn)題說(shuō)明和修改建議等，幫助用戶快速解決問(wèn)題。
Polyspace中MISRAC 2012統(tǒng)計(jì)
Polyspace對(duì)不符合MISRA C的代碼精確定位，并給出詳細(xì)條目、相關(guān)幫助
Formal verification/ Formal proof/ Static analysis of run time error behavior（形式化驗(yàn)證、證明和靜態(tài)分析）
附錄表格中多處提到，高等級(jí)的軟件需要做形式化驗(yàn)證，靜態(tài)分析。其中B.8第9條，要求高等級(jí)的軟件需要進(jìn)行靜態(tài)分析，識(shí)別出軟件中的運(yùn)行時(shí)錯(cuò)誤。Polyspace Bug Finder使用靜態(tài)分析的方法，可以識(shí)別出軟件可能的運(yùn)行時(shí)錯(cuò)誤。Bug Finder能夠提供1 大類，258種錯(cuò)誤，包括關(guān)鍵的數(shù)據(jù)訪問(wèn)沖突、數(shù)組越界和野指針等嚴(yán)重的運(yùn)行時(shí)錯(cuò)誤。
用戶可以根據(jù)依據(jù)情況定義檢查內(nèi)容
表格A.5第10條，明確要求高級(jí)別的軟件需要進(jìn)行形式化驗(yàn)證，而在表格A.9的第1條，再次要求代碼必須進(jìn)行形式化證明。可見(jiàn)當(dāng)前的功能安全規(guī)范已經(jīng)將形式化的方法提高的新的高度。
Polyspace Code Prove使用形式化方法對(duì)代碼進(jìn)行分析，告知用戶代碼是否存在運(yùn)行時(shí)錯(cuò)誤，并以不同顏色標(biāo)識(shí)出來(lái)。針對(duì)有問(wèn)題的代碼，使用紅色進(jìn)行著色，并對(duì)問(wèn)題提供詳細(xì)的問(wèn)題描述，問(wèn)題發(fā)生的事件圖等。
Reverify changed software module/ Reverify affected software modules (軟件變更后的再驗(yàn)證)
在軟件開(kāi)發(fā)過(guò)程中，需求變更是非常常見(jiàn)的。如果在項(xiàng)目的中后期，代碼的更改必須進(jìn)行全面的分析并做回歸測(cè)試。表格 A.8 的第 2 條和第 3 條就是這方面的要求。為了徹底的分析代碼變更的影響，功能安全軟件的全面的分析很有必要。Polyspace Code Prover access 和 Polyspace Code Prover Server 能夠與常見(jiàn)的自動(dòng)化工具如 Jenkins 集成，當(dāng)回歸測(cè)試的代碼進(jìn)入代碼庫(kù)后，Jenkins會(huì)自動(dòng)構(gòu)建新的分析，并將分析結(jié)果保存到 access 中，團(tuán)隊(duì)其他成員可以查看結(jié)果。如技術(shù)經(jīng)理監(jiān)控當(dāng)前的軟件質(zhì)量目標(biāo)。如果因?yàn)榇a變更引入的新的問(wèn)題，質(zhì)量保證人員根據(jù)分析結(jié)果，分配 JIRA 問(wèn)題單給相關(guān)責(zé)任人。
Limited use of pointers / Limited use of recursion（限制指針和遞歸使用）
規(guī)范在附錄表格 B.1 第 5 條和第 6 條分別限制了在功能安全軟件中對(duì)指針和遞歸的使用，對(duì)于 SIL3/4 級(jí)的軟件，必須遵守的規(guī)定，限制因?yàn)檎Z(yǔ)言復(fù)雜引發(fā)的軟件行為不確定性。MISRA C 中的部分條款已經(jīng)對(duì)指針的限制使用做了規(guī)定。其他方面，polyspace code prover 為提供指針?lè)欠ㄒ玫臋z查，并提供詳細(xì)的證明信息。
在遞歸方面，Polyspace Bug Finder 提供代碼度量，包括代碼的圈復(fù)雜度、遞歸度等，并生成報(bào)告作為產(chǎn)品驗(yàn)證的證物。
Boundary value analysis (邊界值分析)
做過(guò)開(kāi)發(fā)的同學(xué)都知道，大量的錯(cuò)誤是發(fā)生在輸入判定的邊界或輸出范圍的邊界上，尤其是變量超出該類型的邊界，引發(fā)運(yùn)行時(shí)錯(cuò)誤，導(dǎo)致安全事故。雖然針對(duì)各種邊界情況設(shè)計(jì)測(cè)試用例，可以查出更多的軟件錯(cuò)誤。但是始終不能做到對(duì)所有邊界值進(jìn)行全方面掌握。
Polyspace Code Prover 在對(duì)代碼進(jìn)行分析的同時(shí)，會(huì)對(duì)代碼中的所有變量進(jìn)行范圍分析，并給出變量在某個(gè)代碼行處的取值范圍，讓變量的所有可能取值一目了然。
Control flow analysis （控制流分析）
一方面，Polyspace Code Prover 在進(jìn)行代碼分析時(shí)，灰色的代碼表示代碼不可達(dá)，表明代碼的控制流存在問(wèn)題。另一方面，Polyspace Code Prover 能夠提取驗(yàn)證 C 代碼中的控制流信息并生成調(diào)用樹(shù)，讓用戶能夠一目了然了解到當(dāng)前軟件的控制流情況。Polyspace Code Prover 能夠?yàn)橄到y(tǒng)函數(shù)調(diào)用關(guān)系生成報(bào)告。
調(diào)用結(jié)構(gòu)報(bào)告
Data flow analysis（數(shù)據(jù)流分析）
Polyspace Code Prover 依據(jù)抽象演繹法對(duì)代碼進(jìn)行代碼靜態(tài)分析，在分析中，包含對(duì)代碼的動(dòng)態(tài)屬性進(jìn)行驗(yàn)證，也就是針對(duì)代碼中的每個(gè)變量的在代碼中的數(shù)據(jù)流確定其動(dòng)態(tài)屬性，Code Prover 依據(jù)數(shù)據(jù)流，對(duì)代碼進(jìn)行演繹分析，并能夠?qū)?shù)據(jù)的訪問(wèn)情況以樹(shù)狀結(jié)構(gòu)表示出來(lái)。
Polyspace Code Prover 提供的變量訪問(wèn)數(shù)
Polyspace通過(guò)TüV SüD認(rèn)證
使用 IEC Certification Kit，幫助用戶快速通過(guò) Polyspace 認(rèn)證。IEC Certification Kit 提供了工具認(rèn)證工件、證書(shū)和測(cè)試套件，并生成可跟蹤性矩陣。該工具包幫助您驗(yàn)證 Polyspace，并簡(jiǎn)化嵌入式系統(tǒng)到 IEC 62304 的認(rèn)證中。
Polyspace 的 TüV SüD 認(rèn)證
認(rèn)證報(bào)告指出，形式化工具Polyspace的使用，可以降低測(cè)試覆蓋度要求。
總結(jié)
醫(yī)療器械的功能安全一直是生產(chǎn)商至始至終繞不開(kāi)的話題，也是生產(chǎn)商最基本的企業(yè)責(zé)任之一。但是這個(gè)企業(yè)責(zé)任確實(shí)不好做，尤其是，隨著醫(yī)療器械的電氣化程度越來(lái)越高，軟件復(fù)雜度指數(shù)級(jí)增加。那么企業(yè)如何面對(duì)這些嚴(yán)峻的問(wèn)題? Polyspace 給出了這樣一份答卷。它能夠幫助您查找軟件中的缺陷，證明您的軟件系統(tǒng)沒(méi)有運(yùn)行時(shí)錯(cuò)誤，并且支持您將它作為 IEC 62304 認(rèn)證的工具，獲得 FDA/CE 的認(rèn)證。
