程序中死鎖檢測(cè)的方法和工具

翟宇鵬，程雪梅

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都610065）

程序中死鎖檢測(cè)的方法和工具

翟宇鵬，程雪梅

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都610065）

死鎖一直都是并發(fā)系統(tǒng)中最重要的問(wèn)題之一，對(duì)死鎖檢測(cè)的研究一直都在不斷地進(jìn)行著。模型檢測(cè)方法是一種重要的自動(dòng)驗(yàn)證技術(shù)，越來(lái)越多地被用在驗(yàn)證軟硬件設(shè)計(jì)是否規(guī)范的工作中。針對(duì)死鎖檢測(cè)的問(wèn)題進(jìn)行綜述，統(tǒng)計(jì)已有的死鎖檢測(cè)方法的文獻(xiàn)資料并給出統(tǒng)計(jì)結(jié)果。然后對(duì)搜集出來(lái)的文獻(xiàn)進(jìn)行分析，介紹許多動(dòng)態(tài)以及靜態(tài)的死鎖檢測(cè)方法。最后介紹兩種常用的模型檢測(cè)工具，提出使用模型檢測(cè)工具進(jìn)行死鎖檢測(cè)的思路與方法，并證實(shí)這種方法的可行性。

死鎖檢測(cè)；模型檢測(cè)；文獻(xiàn)計(jì)量分析

0 引言

隨著計(jì)算機(jī)行業(yè)的不斷發(fā)展，軟件規(guī)模和復(fù)雜度也在不斷擴(kuò)大，軟件故障已成為計(jì)算機(jī)系統(tǒng)出錯(cuò)和崩潰的主要因素。死鎖[1]是分布式系統(tǒng)以及集成式系統(tǒng)中的最重要的問(wèn)題之一，也是影響軟件安全的主要因素。死鎖會(huì)導(dǎo)致程序無(wú)法正常運(yùn)行或終止，甚至導(dǎo)致系統(tǒng)崩潰，帶來(lái)不必要的損失。同時(shí)，死鎖的運(yùn)行狀態(tài)空間過(guò)大，難于重現(xiàn)和修正等問(wèn)題使其成為軟件領(lǐng)域的難題之一，因此，如何有效地檢測(cè)死鎖,提高軟件的可靠性和安全性，成為急需解決的問(wèn)題。

本文針對(duì)10年內(nèi)國(guó)內(nèi)外各知名數(shù)據(jù)庫(kù)中與死鎖檢測(cè)以及模型檢測(cè)相關(guān)的論文進(jìn)行查詢、篩選、分類、比較、整理等，然后對(duì)整理好的論文進(jìn)行總結(jié)，分析出死鎖檢測(cè)的方法并進(jìn)行羅列比較，以及模型檢測(cè)的工具以及方法，從而再將二者結(jié)合，找出模型檢測(cè)工具在死鎖檢測(cè)里的應(yīng)用。

1 文獻(xiàn)計(jì)量分析

對(duì)搜索出來(lái)的412篇論文的不同方向進(jìn)行了計(jì)量分析，并對(duì)統(tǒng)計(jì)的數(shù)據(jù)進(jìn)行了描述，以及通過(guò)計(jì)量分析來(lái)找出這方面研究領(lǐng)域的熱點(diǎn)。。

因?yàn)榻?0年的論文更能體現(xiàn)出研究的正確方向，所以對(duì)于論文時(shí)間進(jìn)行分析，得知最近10年每年論文發(fā)表量隨著時(shí)間在平緩地增多，可知對(duì)于這方面問(wèn)題的研究總體保持在增長(zhǎng)的狀態(tài)。

對(duì)作者進(jìn)行統(tǒng)計(jì)，分析得知高產(chǎn)的作者只占少數(shù)，只有少數(shù)的作者對(duì)這方面領(lǐng)域的研究比較深入，提出的觀點(diǎn)也具有指導(dǎo)的意義。

對(duì)論文的引文類型的進(jìn)行分析，得知絕大多數(shù)來(lái)自會(huì)議論文或者期刊論文。這也屬于一般的論文來(lái)源規(guī)律，指導(dǎo)研究者應(yīng)該在什么地方查閱文獻(xiàn)或者將文獻(xiàn)發(fā)布在什么地方。

對(duì)論文中關(guān)鍵詞進(jìn)行了統(tǒng)計(jì)，其中系統(tǒng)恢復(fù)最多出現(xiàn)，因?yàn)樗梨i是系統(tǒng)中常出現(xiàn)的一類漏洞，系統(tǒng)恢復(fù)的過(guò)程也就包含了對(duì)死鎖進(jìn)行檢測(cè)并處理的過(guò)程。關(guān)鍵詞中常出現(xiàn)的也包括算法一詞，這也表示對(duì)于死鎖的檢測(cè)，很多人都提出了相應(yīng)的算法。除了算法，另一個(gè)常出現(xiàn)的詞則是分布式，這也是因?yàn)樵诜植际较到y(tǒng)中死鎖檢測(cè)越來(lái)越多，也越來(lái)越被研究者們關(guān)注。

圖1 Refviz分析結(jié)果（matrix圖）

通過(guò)使用Refviz工具，對(duì)關(guān)鍵詞共現(xiàn)頻率進(jìn)行了分析，如圖1，發(fā)現(xiàn)distribute，deadlocks，algorithm共現(xiàn)的頻率最高，這也表面死鎖檢測(cè)方面的研究熱點(diǎn)主要為分布式系統(tǒng)中死鎖檢測(cè)的算法一塊。另外，model與deadlock也有著較高的共現(xiàn)頻率，表明有作者也在提出將模型應(yīng)用在死鎖檢測(cè)中，為文章后面提出的使用模型檢測(cè)方法進(jìn)行死鎖檢測(cè)提供了一些理論的依據(jù)。

2 死鎖檢測(cè)方法

針對(duì)死鎖產(chǎn)生的必要條件，以及不同系統(tǒng)不同程序中的死鎖，許多學(xué)者都提出了新的進(jìn)行死鎖檢測(cè)的方法，或是對(duì)常用方法的改良補(bǔ)充。這篇文章收集了許多不同的死鎖檢測(cè)方法，并簡(jiǎn)單的將它們分為2類，即靜態(tài)方法與動(dòng)態(tài)方法。這一章節(jié)對(duì)其中的一些方法進(jìn)行了闡述，并做了簡(jiǎn)單的分類比較。

2.1 靜態(tài)死鎖檢測(cè)方法

（1）SystemC中的靜態(tài)死鎖檢測(cè)分析方法

SystemC是一種基于C++語(yǔ)言的用于系統(tǒng)設(shè)計(jì)的計(jì)算機(jī)語(yǔ)言。Mikhail Moiseev對(duì)此提出了一個(gè)基于對(duì)靜態(tài)代碼的分析的方法來(lái)解決死鎖的檢測(cè)問(wèn)題[2]。

此方法運(yùn)用了正式的程序模型，為了對(duì)算法進(jìn)行有效的分析，由原理可知唯一的死鎖狀態(tài)是在一個(gè)事件中無(wú)窮的wait都不會(huì)被notify。死鎖會(huì)導(dǎo)致所有程序執(zhí)行的阻塞或者某一部分程序執(zhí)行的阻塞，針對(duì)這兩種情況需要不同的死鎖檢測(cè)規(guī)則。

（2）SHIM并發(fā)語(yǔ)言中的靜態(tài)死鎖檢測(cè)算法

隨著多核處理器的出現(xiàn)，并發(fā)程序也就自然而然的出現(xiàn)，在并發(fā)程序中，兩個(gè)最被關(guān)注的方面就是數(shù)據(jù)爭(zhēng)用（data race）以及死鎖。對(duì)于SHIM語(yǔ)言，它通過(guò)避免共享內(nèi)存從而避免了數(shù)據(jù)爭(zhēng)用的出現(xiàn)，但是卻不能避免死鎖。

Nalini Vasudevan針對(duì)這一問(wèn)題提出了一個(gè)基于模型檢測(cè)的死鎖檢測(cè)技術(shù)，在這個(gè)方法中，建立了SHIM程序的異步抽象模型，并用NuSMV符號(hào)模型檢測(cè)器來(lái)檢測(cè)模型中是否存在死鎖，這個(gè)方法能在系統(tǒng)運(yùn)行前找到系統(tǒng)中存在的潛在的死鎖。

2.2 動(dòng)態(tài)死鎖檢測(cè)

（1）分布式系統(tǒng)中的死鎖檢測(cè)算法

死鎖檢測(cè)是分布式系統(tǒng)中最重要的問(wèn)題之一，Mehdi Hashemzadeh以及他的團(tuán)隊(duì)基于此提出了一個(gè)分布式的死鎖檢測(cè)算法[3]：該算法通過(guò)探針進(jìn)行標(biāo)記，對(duì)每個(gè)節(jié)點(diǎn)進(jìn)行進(jìn)行檢測(cè)，通過(guò)層層條件來(lái)找出死鎖。該算法能通過(guò)死鎖中包含的節(jié)點(diǎn)來(lái)管理算法同時(shí)運(yùn)行于幾處，可以防止對(duì)同一處死鎖進(jìn)行多次檢測(cè)，可以通過(guò)對(duì)進(jìn)程進(jìn)行優(yōu)先級(jí)劃分來(lái)來(lái)最小化算法同時(shí)運(yùn)行于幾處時(shí)產(chǎn)生的無(wú)用的信息。同時(shí)這個(gè)算法通過(guò)其獨(dú)特的特性，能在死鎖被檢測(cè)出來(lái)的同時(shí)進(jìn)行解決。

除了Mehdi Hashemzadeh提出的算法，對(duì)于分布式系統(tǒng)中的死鎖檢測(cè)問(wèn)題，還有幾位其他作者也提出了不同的方法。

（2）并發(fā)的消息傳遞程序中的死鎖檢測(cè)算法

針對(duì)于并發(fā)消息傳遞程序中的死鎖問(wèn)題，Sagar Chaki以及他的團(tuán)隊(duì)提出了一種算法，并且此算法采用了包括抽象型以及組合型的論證的框架，有效的解決了因死鎖引起的狀態(tài)空間爆炸的問(wèn)題[4]。此算法使用了抽象、驗(yàn)證、精確的三步迭代過(guò)程來(lái)檢測(cè)系統(tǒng)中是否存在死鎖。Chaki指出此算法在將來(lái)還能用假設(shè)-證明式（assume-guarantee style）的推論來(lái)進(jìn)行提升，同時(shí)他的團(tuán)隊(duì)也將在未來(lái)做這方面的研究。

（3）Java多線程程序中的死鎖檢測(cè)方法

Java語(yǔ)言由于其被用戶越來(lái)越廣泛的使用，它里面的死鎖檢測(cè)也就變得重要。

Takao Shimomura[5]提出了對(duì)Java多線程程序中的死鎖的檢測(cè)方法，提出了3種死鎖的狀態(tài)：鎖阻塞（lock-blocked）、等待阻塞（wait-blocked）、加入阻塞（join-blocked），在這3個(gè)死鎖狀態(tài)的基礎(chǔ)上將死鎖分為了2種類型：環(huán)型以及非環(huán)型。Takao還對(duì)他提出的3種死鎖狀態(tài)進(jìn)行了實(shí)驗(yàn)，較好地檢測(cè)出了他提出的死鎖。

對(duì)于Java中的死鎖檢測(cè)問(wèn)題，Yan Wen[6]也提出了名為JDeadlockDetector的新的Java線程死鎖檢測(cè)的方法。

（4）過(guò)程網(wǎng)絡(luò)（Process Network）中的死鎖檢測(cè)算法

過(guò)程網(wǎng)絡(luò)模型用于為并行程序設(shè)計(jì)設(shè)計(jì)語(yǔ)言，因?yàn)槠渲С譄o(wú)限通道的能力而成為了基于流的多媒體應(yīng)用以及信號(hào)處理應(yīng)用的理想模型[7]，然而在實(shí)現(xiàn)它的過(guò)程中卻出現(xiàn)了死鎖的問(wèn)題。Mar'ia Castillo在論文中介紹了一種復(fù)雜度為O（n）的算法去解決死鎖，為了減少信息的數(shù)量，該算法從系統(tǒng)轉(zhuǎn)變成死鎖狀態(tài)的過(guò)程中提取信息，并能保證檢測(cè)出死鎖所在的節(jié)點(diǎn)。

（5）運(yùn)用幾何學(xué)進(jìn)行死鎖檢測(cè)

David A.Cape[8]提出了一種運(yùn)用包含拓?fù)涓拍畹膸缀螌W(xué)知識(shí)將狀態(tài)空間分成幾個(gè)部分，并通過(guò)對(duì)狀態(tài)空間的減少進(jìn)行研究，從而對(duì)死鎖問(wèn)題進(jìn)行解決。以前對(duì)狀態(tài)空間都是進(jìn)行歸納性的劃分，而他則展示了一種由遞歸方法促進(jìn)的分解方法，這種方法能有效的減少狀態(tài)轉(zhuǎn)換的規(guī)模，從而能整體提升驗(yàn)證的運(yùn)行效率。

3 基于模型檢測(cè)工具的死鎖檢測(cè)方法

模型檢測(cè)是一種很重要的自動(dòng)驗(yàn)證技術(shù)，一般應(yīng)用于驗(yàn)證系統(tǒng)設(shè)計(jì)是否滿足設(shè)計(jì)規(guī)范。模型檢測(cè)方法最早由Allen Emerson[9]等人分別獨(dú)立提出，其基本思想是先建立待驗(yàn)證系統(tǒng)的有限狀態(tài)模型，然后使用算法對(duì)模型中的所有可能執(zhí)行組合狀態(tài)進(jìn)行窮盡搜索，通過(guò)利用驗(yàn)證表達(dá)式判斷這些組合路徑是否符合設(shè)計(jì)規(guī)范，如果某條執(zhí)行路徑不滿足設(shè)計(jì)規(guī)范，模型檢測(cè)工具會(huì)給出不滿足該設(shè)計(jì)規(guī)范的執(zhí)行路徑[10]。雖然模型檢測(cè)在現(xiàn)階段起著越來(lái)越重要的作用，但它也有著它的弊端，當(dāng)系統(tǒng)或者軟件的模塊很多時(shí)，所能產(chǎn)生的狀態(tài)組合也會(huì)以指數(shù)倍數(shù)增長(zhǎng)，導(dǎo)致檢測(cè)的難度會(huì)大大的增加。

模型檢測(cè)是一種很重要的自動(dòng)驗(yàn)證技術(shù)，而死鎖檢測(cè)是一種在如今的軟件系統(tǒng)中很重要的問(wèn)題，本章節(jié)將討論到將這二者結(jié)合起來(lái)，使用模型檢測(cè)的工具來(lái)對(duì)死鎖進(jìn)行檢測(cè)，從中發(fā)現(xiàn)對(duì)死鎖這一問(wèn)題的另一種方面的解決辦法。

3.1 模型檢測(cè)工具介紹

模型檢測(cè)有許許多多的方法與工具，而這其中最被人們熟知的工具之一是NuSMV[11]。它是一款模型檢測(cè)工具，它在SMV（Symbolic Model Checker）工具的基礎(chǔ)上進(jìn)行改進(jìn)后產(chǎn)生，具有了一般的模型檢測(cè)工具有的所有功能，功能較SMV更為強(qiáng)大。NuSMV是由多個(gè)模塊構(gòu)建組成，模塊與模塊之間相互獨(dú)立，它們通過(guò)模塊的內(nèi)部接口來(lái)進(jìn)行通信。同時(shí)NuSMV是一個(gè)開(kāi)源的工具，它允許使用者對(duì)其進(jìn)行擴(kuò)展修改，這就使得NuSMV被廣泛的應(yīng)用在了許多研究的領(lǐng)域。NuSMV高效的實(shí)現(xiàn)了符號(hào)模型檢測(cè)技術(shù)[12]，它是第一款基于CUDD包中的[13]BBDs（Binary Decision Diagrams）操作的模型檢測(cè)工具。NuSMV在模型檢測(cè)中是一個(gè)比較經(jīng)典的工具，對(duì)符號(hào)化模型檢測(cè)算法進(jìn)行了優(yōu)化，達(dá)到了高效驗(yàn)證的目標(biāo)，并且NuSMV的軟件體系結(jié)構(gòu)設(shè)計(jì)的比較靈活，容易對(duì)功能進(jìn)行擴(kuò)展。

NuSMV的前身是SMV，它對(duì)后者在不同程度上進(jìn)行了優(yōu)化，包括功能的擴(kuò)展、系統(tǒng)架構(gòu)的優(yōu)化以及易用性的優(yōu)化。

3.2 模型檢測(cè)工具在死鎖檢測(cè)中的應(yīng)用

這一節(jié)提出了一種模型檢測(cè)工具在死鎖檢測(cè)中的應(yīng)用方法，此方法主要用在系統(tǒng)設(shè)計(jì)階段對(duì)設(shè)計(jì)方案進(jìn)行死鎖檢測(cè)，并選擇NuSMV來(lái)進(jìn)行操作。

因?yàn)樗梨i的發(fā)生具有偶發(fā)性，在系統(tǒng)運(yùn)行時(shí)某一些執(zhí)行路徑在特定條件下才會(huì)出現(xiàn)，這樣模型檢測(cè)可以對(duì)所有可能的執(zhí)行路徑進(jìn)行模擬運(yùn)行，將模型檢測(cè)應(yīng)用到死鎖檢測(cè)，對(duì)并發(fā)系統(tǒng)進(jìn)程之間資源使用進(jìn)行執(zhí)行路徑搜索，設(shè)計(jì)合理的時(shí)序邏輯表達(dá)式，可以達(dá)到死鎖檢測(cè)的目的。由于并發(fā)系統(tǒng)在調(diào)用資源時(shí)，調(diào)用的進(jìn)程順序具有不確定性，而狀態(tài)組合又是有限狀態(tài)，因此可以對(duì)系統(tǒng)進(jìn)行建模，通過(guò)NuSMV工具驗(yàn)證時(shí)序邏輯表達(dá)式的正確性來(lái)判斷是否發(fā)生死鎖。

針對(duì)并發(fā)同步和異步以及這兩種模式下的信號(hào)量、互斥鎖、條件變量機(jī)制設(shè)計(jì)出了8個(gè)基于NuSMV的死鎖檢測(cè)模型驗(yàn)證模板，通過(guò)對(duì)被測(cè)系統(tǒng)的設(shè)計(jì)文檔分析獲得并發(fā)進(jìn)程對(duì)臨界區(qū)的訪問(wèn)信息，使用算法自動(dòng)對(duì)這些信息判斷處理并創(chuàng)建用于驗(yàn)證是否發(fā)生死鎖的時(shí)序邏輯表達(dá)式，然后根據(jù)獲得的信息選擇相應(yīng)模板轉(zhuǎn)換為NuSMV可以運(yùn)行的SMV程序，之后利用NuSMV對(duì)時(shí)序邏輯表達(dá)式進(jìn)行驗(yàn)證，通過(guò)時(shí)序邏輯表達(dá)式真值判斷是否產(chǎn)生死鎖，并給出真值為假的執(zhí)行路徑，該路徑就是產(chǎn)生死鎖時(shí)的進(jìn)程執(zhí)行路徑。最終通過(guò)基于NuSMV死鎖檢測(cè)模型驗(yàn)證模板和算法實(shí)現(xiàn)并發(fā)同步和異步以及這兩種模式下的信號(hào)量、互斥鎖、條件變量機(jī)制的死鎖檢測(cè)。

4 結(jié)語(yǔ)

本文對(duì)死鎖檢測(cè)的問(wèn)題以及模型檢測(cè)方法進(jìn)行了綜述，羅列出了現(xiàn)有的比較常見(jiàn)比較被人們熟知的方法，并對(duì)它們的特性等進(jìn)行了描述。文章能夠給未來(lái)進(jìn)行這方面研究的研究人員帶來(lái)幫助，讓他們能夠減少自己重新查閱這方面文獻(xiàn)資料并搜集需要信息的工作，將重點(diǎn)放在進(jìn)行新的死鎖檢測(cè)方法的研究以及對(duì)已有方法進(jìn)行完善的工作上面。同時(shí)這篇文章也提出了一種新的進(jìn)行死鎖檢測(cè)的思路，這一思路也得到了實(shí)驗(yàn)結(jié)果的支持，表明這個(gè)方法確實(shí)是有效的，但卻還需要更進(jìn)一步的深入實(shí)驗(yàn)。

死鎖是很難避免發(fā)生的缺陷，隨著科技的發(fā)展，越來(lái)越多新穎卻讓人眼前一亮的方法出現(xiàn)，這些方法或者從整體提升了整個(gè)死鎖檢測(cè)的效率，或者對(duì)某一方面的死鎖檢測(cè)進(jìn)行了很好的優(yōu)化。雖然死鎖不會(huì)因?yàn)檫@些方法得到徹底的解決，但這些不同研究者的不同的思路卻讓人相信死鎖的問(wèn)題會(huì)得到很好的處理。

[1]A.O.Abd El-Gwad,A.I.Saleh,M.M.Abd-ElRazik.A Novel Scheduling Strategy for an Efficient Deadlock Detection.In Computer Engineering&Systems,2009.ICCES 2009.International Conference on,2009,pp.579-583.

[2]M.Moiseev,A.Zakharov,I.Klotchkov,S.Salishev.Static Analysis Method for Deadlock Detection in SystemC Designs.In System on Chip（SoC）,2011 International Symposium on,2011,pp.42-47.

[3]M.Hashemzadeh,N.Farajzadeh,A.T.Haghighat.Optimal Detection and Resolution of Distributed Deadlocks in the Generalized Model.in Parallel,Distributed,and Network-Based Processing,2006.PDP 2006.14th Eurom icro International Conference on,2006, p.4 pp.

[4]S.Chaki,E.Clarke,J.Ouaknine,N.Sharygina.Automated,Compositional and Iterative Deadlock Detection.in Formal Methods and Models for Co-Design,2004.MEMOCODE'04.Proceedings.Second ACM and IEEE International Conference on,2004,pp.201-210.

[5]T.Shimomura，K.Ikeda.Waiting Blocked-Tree Type Deadlock Detection.in Science and Information Conference（SAI）,2013,2013, pp.45-50.

[6]W.Yan,Z.Jinjing,H.Minhuan,C.Hua.Towards Detecting Thread Deadlock in Java Programswith JVM Introspection.in Trust,Security and Privacy in Computing and Communications（TrustCom）,2011 IEEE 10th International Conference on,2011,pp.1600-1607.

[7]M.Castillo,F.Farina,A.Cordoba.Deadlock in Process Networks:A Dynamic Detection and Resolution.in Signal Processing and Communication Systems（ICSPCS）,2011 5th International Conference on,2011,pp.1-9.

[8]D.A.Cape,S.C.Jackson,B.M.McMillin.Dihomotopic Deadlock Detection via Progress Shell Decomposition.in Advances in System Testing and Validation Lifecycle（VALID）,2010 Second International Conference on,2010,pp.20-25.

[9]C.E，E.E.Design and Synthesis of Synchronization Skeletons Using Braching Time Temporal Locic.LNUS 137,pp.337-351,1982.

[10]E.M.Clarke，O.Grumberg.Counterexample Guided Abstraction Refinement for Symbolic Model Checking.Journal of the ACM,vol.50（5）,pp.752-794,2003.

[11]K.L.，McMillall.Symbolic Model Checking.Kluwer Academ ic Publ,1993.

[12]R.Cavada.,A.Cimatti.,C.A.Jochim.,G.Keighren.,E.Olivetti.,M.Pistore.,etal..NuSMV2.5.4-User Mannual,"IRST,2005.

[13]顧濱兵.基于模型檢測(cè)的軟件驗(yàn)證技術(shù)研究[D].吉林大學(xué)學(xué)報(bào),2007.

Methods and Tools of Program Dead lock Detection

ZHAIYu-peng，CHENG Xue-mei

（College of Computer Science,Sichuan University,Chengdu 610065）

Deadlock is always one of themost important problems in concurrent system,and the study of deadlock detection has never been stopped. Model checking is an important technology of automatic verification,is increasingly being used in the verification of software and hardware design of whether the specification.Reviews on the problems aiming at deadlock detection,first reviews the deadlock detection method of statisticalwork,the existing literature and gives the statistical results.Then analyzes the collection of literature,proposes the dynamic as well as static dead lock detection method.Finally,introduces two kinds of common model checking tools,and then describes the use ofmodel checking tool of thoughts andmethods for the detection of deadlocks,and confirms the feasibility of thismethod.

Dead lock Detection;Model Checking;Literature Measurement Analysis

1007-1423（2017）03-0041-04

10.3969/j.issn.1007-1423.2017.03.011

翟宇鵬（1992-），男，江蘇興化人，碩士研究生，研究方向?yàn)榍度胧杰浖_(kāi)發(fā)與測(cè)試

2016-11-22

2017-01-15

四川省應(yīng)用基礎(chǔ)研究項(xiàng)目（No.2014JY0112）

程雪梅（1991-），女，重慶萬(wàn)州人，碩士，研究方向?yàn)檐浖こ膛c軟件測(cè)試