模型檢測(cè)技術(shù)在程序內(nèi)存泄漏檢測(cè)中的應(yīng)用

陳宇星

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

模型檢測(cè)技術(shù)在程序內(nèi)存泄漏檢測(cè)中的應(yīng)用

陳宇星

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

軟件開(kāi)發(fā)常用的動(dòng)態(tài)內(nèi)存管理技術(shù)雖然使得程序的設(shè)計(jì)更靈活卻很容易造成內(nèi)存管理漏洞，特別是內(nèi)存泄漏問(wèn)題。內(nèi)存泄漏的堆積會(huì)導(dǎo)致程序運(yùn)行異常甚至崩潰，因此內(nèi)存泄漏檢測(cè)是一個(gè)長(zhǎng)期熱門(mén)的研究課題。而模型檢測(cè)技術(shù)是基于對(duì)程序所有可能執(zhí)行路徑的盡可能地仿真來(lái)檢測(cè)出程序中潛在的漏洞，所以可以將模型檢測(cè)技術(shù)用于程序內(nèi)存泄漏檢測(cè)中。采用系統(tǒng)化文獻(xiàn)綜述的方法歸納總結(jié)應(yīng)用模型檢測(cè)技術(shù)的內(nèi)存泄漏檢測(cè)方法和工具。

內(nèi)存泄漏檢測(cè)；模型檢測(cè)；內(nèi)存錯(cuò)誤；系統(tǒng)文獻(xiàn)綜述

0 引言

現(xiàn)階段的動(dòng)態(tài)內(nèi)存機(jī)制雖然使得程序的設(shè)計(jì)更靈活和方便，但這個(gè)機(jī)制很容易造成內(nèi)存錯(cuò)誤，其中內(nèi)存泄漏又是最難檢測(cè)并定位的。因此，如何有效檢測(cè)程序中的內(nèi)存泄漏是一個(gè)長(zhǎng)期熱門(mén)的研究課題。內(nèi)存泄漏（Memory Leak）是由于程序在運(yùn)行過(guò)程中動(dòng)態(tài)分配的內(nèi)存不再使用了卻沒(méi)有被及時(shí)釋放造成的[1]。在這種情況下，程序不斷的運(yùn)行，泄漏的內(nèi)存會(huì)不斷地增加，程序的性能也會(huì)因此而不斷下降，甚至程序會(huì)由于內(nèi)存被耗盡而崩潰。對(duì)于嵌入式系統(tǒng)這類(lèi)內(nèi)存有限的系統(tǒng)或者服務(wù)器這類(lèi)會(huì)運(yùn)行很長(zhǎng)時(shí)間的系統(tǒng)來(lái)說(shuō),內(nèi)存泄漏是個(gè)十分嚴(yán)重的缺陷。因此盡早地檢測(cè)到并處理程序中的內(nèi)存泄漏問(wèn)題是十分必要的。

模型檢測(cè)（Model Checking）技術(shù)是一種通過(guò)窮舉搜索有限狀態(tài)空間來(lái)實(shí)現(xiàn)對(duì)模型的檢測(cè)的自動(dòng)驗(yàn)證技術(shù)，已經(jīng)越來(lái)越被重視并將其應(yīng)用到了廣泛的范圍當(dāng)中[2]。因此這篇論文著重對(duì)模型檢測(cè)技術(shù)在C/C++程序中的內(nèi)存泄漏檢測(cè)的應(yīng)用進(jìn)行了綜述分析。為研究學(xué)者們下一步的研究課題提供綜合性的參考，也能為工業(yè)界應(yīng)用這個(gè)領(lǐng)域的技術(shù)提出一個(gè)決策的依據(jù)。

1 研究方法

系統(tǒng)文獻(xiàn)綜述(Systematic Literature Review)又被稱作系統(tǒng)評(píng)價(jià)，是一種針對(duì)某一研究問(wèn)題開(kāi)展的基于文獻(xiàn)的系統(tǒng)化綜述方法[3]。一開(kāi)始主要用于醫(yī)學(xué)領(lǐng)域以及社會(huì)學(xué)研究領(lǐng)域，在2004年被引入了軟件工程領(lǐng)域，系統(tǒng)綜述主要包含了3個(gè)階段[3]:

（1）制定計(jì)劃

在這個(gè)階段對(duì)綜述的需求進(jìn)行分析，并確定開(kāi)展此綜述的目的，然后設(shè)計(jì)出展開(kāi)綜述的步驟方案，以便引導(dǎo)后續(xù)的工作。主要要分以下三步：

①提出研究問(wèn)題

問(wèn)題1：現(xiàn)有的應(yīng)用了模型檢測(cè)技術(shù)的內(nèi)存泄漏檢測(cè)方法和工具有哪些？

問(wèn)題2：模型檢測(cè)技術(shù)在內(nèi)存泄漏檢測(cè)上應(yīng)用的不足和發(fā)展前景？

②檢索策略

這篇論文用于分析的數(shù)據(jù)來(lái)源于IEEE Xplore，Web of Science、ACM以及CNKI等數(shù)據(jù)庫(kù)。檢索詞包括：“內(nèi)存泄漏”、“模型檢測(cè)”、“內(nèi)存錯(cuò)誤”、“memory leak”、“model checking”、“memory error”。

③篩選原則

對(duì)于檢索出來(lái)的文獻(xiàn)通過(guò)其發(fā)表年限、被引用次數(shù)、發(fā)表期刊、篇幅以及主題是否是關(guān)于模型檢測(cè)技術(shù)在內(nèi)存泄漏檢測(cè)中的應(yīng)用來(lái)決定是否將其錄入最終用來(lái)分析的論文庫(kù)。

（2）執(zhí)行計(jì)劃

這個(gè)階段按第一步制定的檢索策略和篩選原則來(lái)收集能夠回答研究問(wèn)題的文獻(xiàn)并進(jìn)行數(shù)據(jù)提取與分析。最終檢索到的文獻(xiàn)通過(guò)第一步消重，刪除掉錄入Endnote中的重復(fù)論文后共有155條記錄；第二步通過(guò)閱讀題目和摘要來(lái)過(guò)濾與研究主題不相關(guān)的論文；第三步刪除掉短文和引用次數(shù)很少的論文。通過(guò)以上步驟，最終確定選入的文獻(xiàn)共53篇。

（3）完成文獻(xiàn)綜述報(bào)告

最終被錄入的研究，按照文獻(xiàn)綜述的需求來(lái)提取數(shù)據(jù)，對(duì)所獲得的數(shù)據(jù)進(jìn)行歸納分析,并對(duì)結(jié)果給出解釋。最終整個(gè)綜述過(guò)程和結(jié)果，形成研究報(bào)告。

2 研究結(jié)果

基于模型檢測(cè)的內(nèi)存泄漏檢測(cè)通常是對(duì)被測(cè)程序進(jìn)行語(yǔ)法、詞法分析，然后使用模型檢測(cè)算法來(lái)判斷分析后的結(jié)果。而各種方法用于分析的程序的形式不同，有些方法是直接分析被測(cè)程序的源代碼，有些方法是分析被測(cè)程序的匯編語(yǔ)言形式的代碼，但他們獲得匯編代碼的方式又可能不同，例如MLAB框架和X86EBMC工具，它們分析的匯編代碼是由被測(cè)程序的可執(zhí)行文件經(jīng)過(guò)反匯編后獲得的，而LLBMC工具則是通過(guò)編譯被測(cè)程序的源代碼來(lái)獲得匯編代碼的。各種內(nèi)存泄漏檢測(cè)方法使用的模型檢測(cè)方法和工具也不盡相同。

2.1 基于模型檢測(cè)的內(nèi)存泄漏檢測(cè)方法

（1）TMC（Type and Model Checking）

TMC是一種結(jié)合了類(lèi)型分析技術(shù)和模型檢測(cè)技術(shù)的檢測(cè)內(nèi)存泄漏的靜態(tài)分析方法，利用模型檢測(cè)來(lái)對(duì)使用類(lèi)型分析方法得出的結(jié)果進(jìn)行更仔細(xì)的檢查[4]。TMC方法首先是通過(guò)類(lèi)型分析來(lái)獲得程序的控制流圖和數(shù)據(jù)流信息（如別名分析），然后分析出的結(jié)果就會(huì)作為模型檢測(cè)分析的對(duì)象輸入模型檢測(cè)模塊[4]。最終得出檢測(cè)結(jié)果。TMC通過(guò)將模型檢測(cè)方法與類(lèi)型分析方法的優(yōu)點(diǎn)結(jié)合起來(lái)，可以獲得比單用類(lèi)型分析方法更為準(zhǔn)確的結(jié)果[4]。但是其分析工具功能還不夠完善，還不能有效地對(duì)大型軟件系統(tǒng)進(jìn)行屬性檢查。

（2）MLAB(Memory Leak Analysis for Binaries)

MLAB是用于檢測(cè)二進(jìn)制可執(zhí)行文件中的內(nèi)存泄漏漏洞的框架方案，它能把二進(jìn)制形式的代碼恢復(fù)成同機(jī)器不相干的編譯中間表示形式，還能將程序中的控制流與數(shù)據(jù)流信息恢復(fù)過(guò)來(lái)，然后利用模型檢測(cè)算法來(lái)分析恢復(fù)過(guò)來(lái)的控制流和數(shù)據(jù)流信息，從而檢測(cè)出被測(cè)程序中的內(nèi)存泄漏[5]。MLAB框架中使用了上述TMC算法。MLAB不需要掌握任何與源代碼有關(guān)的信息，僅僅根據(jù)程序的二進(jìn)制形式就可以恢復(fù)程序的控制流和數(shù)據(jù)流信息。MLAB具有不錯(cuò)的可擴(kuò)展性，是對(duì)二進(jìn)制程序?qū)嵤傩苑治龅囊环N常用的方法[5]。

（3）基于SMT的有界模型檢測(cè)方法

2010年，Carsten Sinz等人提出了一種基于有界模型檢測(cè)（BMC）來(lái)檢測(cè)C程序中的內(nèi)存錯(cuò)誤（非法內(nèi)存方法、堆棧溢出、內(nèi)存泄漏、非法釋放等）的方法[6]。這個(gè)方法不是直接在C源碼上檢測(cè)，而是檢測(cè)一種由LLVM（Low Level Virtual Machine）編譯器框架產(chǎn)生的類(lèi)似RISC匯編語(yǔ)言的中介碼。因此這個(gè)方法的分析結(jié)果就跟實(shí)際運(yùn)行程序檢測(cè)到的結(jié)果相近。后端的SMT求解器采用Boolector或者STP工具。后文提到的LLBMC工具采用的是STP工具。LLVM編譯器前端（llvm-gcc）將C程序源代碼轉(zhuǎn)化成LLVM-IR程序，之后把它輸入循環(huán)展開(kāi)/函數(shù)內(nèi)聯(lián)模塊，輸出的結(jié)果是被轉(zhuǎn)化的匯編碼，循環(huán)展開(kāi)以及函數(shù)內(nèi)聯(lián)是由LLVM的庫(kù)提供的代碼完成的，然后將被轉(zhuǎn)化的代碼輸入到邏輯編碼模塊，共同輸入的還有一個(gè)內(nèi)存模型，這個(gè)內(nèi)存模型包含了C程序中的關(guān)于內(nèi)存訪問(wèn)的語(yǔ)義信息。邏輯編碼模塊輸出的位向量和數(shù)組的邏輯形式通過(guò)SMT求解器后輸出驗(yàn)證的結(jié)果以及錯(cuò)誤路徑，這個(gè)錯(cuò)誤報(bào)告是由LLVM的調(diào)試信息模塊產(chǎn)生的。

2.2 基于模型檢測(cè)的內(nèi)存泄漏檢測(cè)工具

（1）CodeAuditor

CodeAuditor[7]是一個(gè)包含了前端預(yù)處理模塊和后端模型檢測(cè)模塊的內(nèi)存泄漏檢測(cè)原型工具。它的實(shí)現(xiàn)原理是將約束分析和模型檢測(cè)技術(shù)相結(jié)合，通過(guò)跟蹤與緩存相關(guān)的變量的內(nèi)存大小并在潛在漏洞點(diǎn)插入約束斷言，這樣就將漏洞檢測(cè)轉(zhuǎn)換成了通過(guò)模型檢測(cè)來(lái)驗(yàn)證這些斷言的可達(dá)性。通過(guò)對(duì)插入了斷言的代碼進(jìn)行程序切片來(lái)減小程序的大小，從而減輕了程序系統(tǒng)狀態(tài)的組合爆炸給模型檢測(cè)帶來(lái)的負(fù)擔(dān)。由于程序切片并沒(méi)有改變切片標(biāo)準(zhǔn)重的變量的值，所以當(dāng)程序被切片時(shí)，斷言的安全將不會(huì)被改變。CodeAuditor基于程序分析和模型檢測(cè)工具BLAST，具有較小的錯(cuò)誤報(bào)警率。

（2）WBoxTool結(jié)合Blast

付曉毓等人提出了一種結(jié)合了靜態(tài)分析、代碼插裝以及模型檢測(cè)技術(shù)的內(nèi)存泄漏故障的靜態(tài)檢測(cè)系統(tǒng)，這個(gè)系統(tǒng)與CodeAuditor框架類(lèi)似。它的主要原理是首先構(gòu)建出指針屬性的約束條件，接著以斷言的形式將其插入到程序源代碼當(dāng)中，這樣檢測(cè)程序中的內(nèi)存泄漏就被轉(zhuǎn)化成了判定源代碼中特定位置的斷言的可達(dá)性[8]。最后使用一個(gè)模型檢測(cè)工具來(lái)判定那些斷言，若判定的結(jié)果是不正確，那么該位置處的代碼就有可能會(huì)造成內(nèi)存泄漏[8]。這個(gè)靜態(tài)檢測(cè)系統(tǒng)由函數(shù)靜態(tài)信息提取模塊、插裝模塊以及模型檢測(cè)模塊等三個(gè)模塊構(gòu)成，其中模型檢測(cè)模塊使用了由UC Berkeley開(kāi)發(fā)的針對(duì)C程序的安全性驗(yàn)證的工具——Blast模型檢測(cè)工具[8]。WBoxTool與Blast工具的結(jié)合雖然在小型實(shí)例程序檢測(cè)上取得了較好的成果，但是要將其應(yīng)用到大規(guī)模的軟件上還遠(yuǎn)遠(yuǎn)不夠。

（3）Goanna

2007年，F(xiàn)ehnker等人開(kāi)發(fā)出了第一個(gè)使用了模型檢測(cè)器NuSMV的C/C++靜態(tài)源碼分析工具——Goanna[9]。那時(shí)的Goanna只是一個(gè)原型工具，它可以分析程序的的部分特性。用戶需要做的僅是提供一個(gè)CTL（Computation Tree Logic）的規(guī)格說(shuō)明并且以查詢語(yǔ)句為單位來(lái)定義這個(gè)規(guī)格說(shuō)明的原子命題（Atomic Proposition）。把程序翻譯成控制流圖、模式匹配、隨后的貼標(biāo)以及報(bào)告錯(cuò)誤，這些過(guò)程都是全自動(dòng)的，大大減小了用戶的負(fù)擔(dān)。盡管Goanna在實(shí)際使用上已經(jīng)足夠，但是其性能仍然有很大的空間有待改善。針對(duì)Goanna中存在的各種問(wèn)題，F(xiàn)ehnker等人在2012年開(kāi)發(fā)出了最新版本的Goanna解決了性能問(wèn)題。并且，最新版的Goanna除了可以執(zhí)行內(nèi)存泄漏檢測(cè)外，還能執(zhí)行超過(guò)250個(gè)有很高價(jià)值的檢查，例如數(shù)組越界、空指針錯(cuò)誤、內(nèi)存損壞、字符串溢出、雙重釋放、安全性缺陷、算數(shù)錯(cuò)誤、可移植性缺陷等[10]。最新開(kāi)發(fā)的Goanna不需要編譯或執(zhí)行被測(cè)程序，只需要分析程序的源代碼就可以自動(dòng)地找到程序中的漏洞，因此在軟件開(kāi)發(fā)生命周期的最早階段就能及時(shí)發(fā)現(xiàn)漏洞，所以，用戶可以在降低開(kāi)發(fā)成本的同時(shí)提高其代碼的質(zhì)量，也節(jié)約了產(chǎn)品開(kāi)發(fā)的時(shí)間，使其能夠更快地進(jìn)入市場(chǎng)。Goanna可以將檢測(cè)到的缺陷通過(guò)一個(gè)方便使用的接口繪制成可視化的報(bào)告。

（4）X86EBMC(X86 Executable Bounded Model Check)

X86EBMC[11]是一個(gè)使用了有界模型檢測(cè)方法的針對(duì)可執(zhí)行文件的模型檢測(cè)工具，能夠檢測(cè)內(nèi)存泄漏、緩存溢出等漏洞。它是反匯編工具IDA Pro的插件，因?yàn)椴捎昧嗣嫦驅(qū)ο蟮姆椒▽?shí)現(xiàn)，因此其可擴(kuò)展性和跨平臺(tái)性的較強(qiáng)。X86EBMC采用LTL線性時(shí)序邏輯來(lái)描述系統(tǒng)的安全屬性，由于模型檢測(cè)器SPIN主要用于檢測(cè)LTL公式的可滿足性，所以X86EBMC采用SPIN作為模型檢測(cè)模塊使用的工具。

（5）LLBMC

2012，Carsten Sinz等人根據(jù)他們?cè)?010年提出的方法，開(kāi)發(fā)了一個(gè)基于有界模型檢測(cè)的靜態(tài)軟件分析工具LLBMC[12]，在2013年，又更新了最新版本的LLBMC。它可以用于查找C程序中的漏洞。LLBMC是全自動(dòng)的，它僅需要極少的前期準(zhǔn)備和用戶交互，囊括了所有的C結(jié)構(gòu)。通過(guò)高度精確地將內(nèi)存訪問(wèn)操作模型化從而找到很難被檢測(cè)到的內(nèi)存錯(cuò)誤，例如內(nèi)存泄漏。由于LLBMC的高精確性，它幾乎沒(méi)有誤報(bào)。

（6）F-soft

F-soft[13-14]是由Ilya Shlyakhter等人開(kāi)發(fā)的一個(gè)原型軟件模型檢測(cè)工具，提供了一系列模型軟件的抽象，并且使用了針對(duì)軟件的自定義的基于SAT（satisfiability）和基于BDD（Binary Decision Diagrams）的有界模型檢測(cè)技術(shù)。主要用于檢測(cè)順序C程序。它除了能檢測(cè)內(nèi)存泄漏漏洞以外，還能檢測(cè)數(shù)組邊界違規(guī)、空指針引用、除零等漏洞。

（7）CMC

Madanlal Musuvathi等人開(kāi)發(fā)了一種模型檢測(cè)工具——CMC[15]，它的特點(diǎn)是直接檢測(cè)C/C++的實(shí)現(xiàn)代碼，而不是像F-soft那樣檢測(cè)一個(gè)系統(tǒng)行為的抽象形式，還有一個(gè)特點(diǎn)是可以保存狀態(tài)以避免重復(fù)的狀態(tài)探索。CMC有兩個(gè)主要的優(yōu)點(diǎn)：減少了錯(cuò)誤的漏報(bào)以及減少了因?yàn)檎`報(bào)而造成的時(shí)間的浪費(fèi)。CMC可以檢測(cè)的漏洞有：指針訪問(wèn)違規(guī)、程序斷言失敗、內(nèi)存泄漏等。

（8）CBMC

CBMC[16]是卡內(nèi)基·梅隆大學(xué)的Edmund Clarke等人開(kāi)發(fā)的一個(gè)形式化驗(yàn)證底層ANSI-C程序的工具。它的驗(yàn)證過(guò)程是高度自動(dòng)的，用戶僅需要輸入BMC的邊界就行。它采用的模型檢測(cè)技術(shù)是基于SAT的有界模型檢測(cè)技術(shù)。CBMC除了可以檢測(cè)內(nèi)存泄漏問(wèn)題外，還能檢測(cè)的錯(cuò)誤有指針安全、數(shù)組越界等。

2.3 基于模型檢測(cè)的內(nèi)存泄漏檢測(cè)方法與工具的比較

表1展示了上述方法和工具的比較。

表1 各模型檢測(cè)工具和方法的對(duì)比

3 結(jié)語(yǔ)

動(dòng)態(tài)內(nèi)存管理機(jī)制方便了內(nèi)存的分配與釋放，但當(dāng)程序結(jié)構(gòu)比較復(fù)雜的時(shí)候,很容易因?yàn)殚_(kāi)發(fā)人員的大意造成邏輯錯(cuò)誤，從而可能會(huì)使得程序產(chǎn)生內(nèi)存泄漏。內(nèi)存泄漏的堆積會(huì)對(duì)程序的性能造成很大的影響，因此有效并及時(shí)地檢測(cè)出程序中潛在的內(nèi)存泄漏是意義深遠(yuǎn)的，它也是確保軟件產(chǎn)品質(zhì)量的必要方式。

本文采用系統(tǒng)化文獻(xiàn)綜述的方法，分析了關(guān)于模型檢測(cè)技術(shù)在內(nèi)存泄漏檢測(cè)中的應(yīng)用方面的成果，綜述分析了應(yīng)用了模型檢測(cè)技術(shù)的內(nèi)存泄漏檢測(cè)方法和工具的基礎(chǔ)結(jié)構(gòu)、應(yīng)用的技術(shù)以及其優(yōu)缺點(diǎn)等方面的信息。同時(shí)也指出了這個(gè)研究領(lǐng)域亟待解決的問(wèn)題以及未來(lái)的研究趨勢(shì)。因此，這篇論文可以為研究學(xué)者們下一步的研究題目提供綜合性的參考，也能為工業(yè)界應(yīng)用這個(gè)領(lǐng)域的技術(shù)提出一個(gè)決策的依據(jù)。

[1]王喆.C/C++代碼內(nèi)存泄漏缺陷檢測(cè)方法研究[C]，2012．

[2]趙振西.一種混合式內(nèi)存泄漏靜態(tài)檢測(cè)方法[J].小型微型計(jì)算機(jī)系統(tǒng),2008:1935-1939.

[3]聶坤明,張莉,樊志強(qiáng).軟件產(chǎn)品線可變性建模技術(shù)系統(tǒng)綜述[J].Journal of Software,2013.

[4]Hu,Y,et al.Hybrid Static Method for Memory Leak Detection[J].Journal of Chinese Computer Systems,2008.

[5]趙振西.一種針對(duì)可執(zhí)行代碼的內(nèi)存泄漏靜態(tài)分析方案[N].中國(guó)科學(xué)技術(shù)大學(xué)學(xué)報(bào),2009.

[6]Sinz,C,S.Falke,and F.Merz.A Precise Memory Model for Low-Level Bounded Model Checking[C].In Proceedings of the 5th International Conference on Systems Software Verification，2010.

[7]Lei,W,Z.Qiang,Z.PengChao.Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking[C].2008 Eighth IEEE International Working Conference on Source Code Analysis and Manipulation(SCAM 2008),2008:165-73.

[8]付曉毓，朱利，顧偉.基于模型檢測(cè)的內(nèi)存泄露靜態(tài)測(cè)試方法[J].微電子學(xué)與計(jì)算機(jī),2010(10):170-173.

[9]Fehnker,A,et al.Model Checking Software at Compile Time[C].Theoretical Aspects of Software Engineering,2007.

[10]Fehnker,A.，R.Huuck.Model Checking Driven Static Analysis for the Real World:Designing and Tuning Large Scale Bug Detection [C].Innovations in Systems and Software Engineering,2013，9(1):45-56.

[11]Tang,Z.-c,et al.Bounded Model Checking Security Properties of Executables[J].Journal of Chinese Computer Systems,2008，29(9): 1674-8.

[12]Merz,F,S.Falke,C.Sinz.LLBMC:Bounded Model Checking of C and C++Programs Using a Compiler IR.in Verified Software: Theories,Tools,Experiments.2012,Springer.146-161.

[13]Ivancic,F,et al.Model Checking C Programs Using F-Soft[C].in Computer Design:VLSI in Computers and Processors,2005.ICCD 2005.Proceedings.2005 IEEE International Conference on.2005.IEEE.

[14]Ivan i,F,et al.F-Soft:Software Verification Platform.in Computer Aided Verification.2005.Springer.

[15]Musuvathi,M,et al.CMC:A Pragmatic Approach to Model Checking Real Code.ACM SIGOPS Operating Systems Review,2002.36 (SI):75-88.

[16]Clarke,E,D.Kroening,and F.Lerda.A Tool for Checking ANSI-C Programs.in Tools and Algorithms for the Construction and Analysis of Systems.2004,Springer.168-176.

The Memory Leak Detections with Model Checking

CHEN Yu-xing

（College of Computer Science,Sichuan University，Chengdu610000）

The popular dynamic memory management technology used in software development makes the design process more flexible,but it is also very likely to cause memory management issues,especially the memory leak problem.Memory leaks can cause abnormal operation or even crash the program,so memory leak detection is a hot research topic for a long time.The model checking technology is based on the detection of all possible execution paths of the program as simulation to detect run-time errors,so model checking can be used in memory leak detection.Therefore,draws on a systematic literature review methods to summarize the existing methods and tools of memory leak detection which uses the model checking technology.

Memory Leak Detection;Model Checking;Memory Error;Systematic Literature Review

1007-1423（2017）04-0053-05

10.3969/j.issn.1007-1423.2017.04.012

陳宇星（1993-），女，四川眉山人，碩士研究生，研究方向?yàn)檐浖詣?dòng)化測(cè)試

2016-11-29

2016-01-13