程序自動(dòng)化調(diào)試的多謂詞開關(guān)方法.pdf

1、程序調(diào)試是軟件開發(fā)過程中最關(guān)鍵的環(huán)節(jié)之一，調(diào)試的開銷將直接影響到軟件的成本和軟件公司的收益。對(duì)于程序員來說，調(diào)試也是一個(gè)非常單調(diào)乏味的工作。因此，程序的自動(dòng)化調(diào)試方法成為了計(jì)算機(jī)領(lǐng)域的熱點(diǎn)課題，得到不同領(lǐng)域眾多研究者的關(guān)注，繼而出現(xiàn)了各種各樣的自動(dòng)化調(diào)試方法，如算法調(diào)試、切片技術(shù)、基于模型調(diào)試、基于概率調(diào)試、基于程序狀態(tài)調(diào)試、Delta調(diào)試等等。
　　 現(xiàn)有的大多數(shù)調(diào)試技術(shù)都是經(jīng)驗(yàn)性的，即依靠專家經(jīng)驗(yàn)和一些啟發(fā)式性質(zhì)。為此，劉詠

2、梅教授分析了要基于第一原理為程序調(diào)試建立一個(gè)精確的理論基礎(chǔ)的重要性。本文研究的起點(diǎn)是張翔宇教授等人提出的一種程序調(diào)試的單謂詞開關(guān)方法，其主要思想是通過改變程序運(yùn)行過程中的一個(gè)謂詞實(shí)例的取值使得原來錯(cuò)誤的程序最終運(yùn)行得到正確的結(jié)果，然后根據(jù)被開關(guān)的謂詞利用切片技術(shù)來確定診斷范圍。但很多情況下，只對(duì)單個(gè)謂詞實(shí)例進(jìn)行開關(guān)并不能夠使程序得到正確的運(yùn)行。針對(duì)單謂詞開關(guān)算法的局限性，本文提出有界調(diào)試的多謂詞開關(guān)算法(bounded debuggin

3、g via multiple predicate switchingalgorithm，BMPS)，通過在程序運(yùn)行過程中開關(guān)多個(gè)謂詞實(shí)例來得到一個(gè)正確的運(yùn)行，且在此運(yùn)行中每個(gè)循環(huán)的執(zhí)行次數(shù)不超過一個(gè)給定的上界。BMPS算法可以通過一個(gè)可滿足性(satisfiability，SAT)求解器來實(shí)現(xiàn)。
　　 文中討論的程序錯(cuò)誤主要為右端(righthandside，RHS)錯(cuò)誤，即錯(cuò)誤出現(xiàn)在控制謂詞或者賦值語句的右邊。對(duì)于只含條件控制

4、語句的程序，本文證明了BMPS算法對(duì)于RHS錯(cuò)誤是準(zhǔn)完備的，即真實(shí)錯(cuò)誤的部分語句一定會(huì)被BMPS算法返回。對(duì)于含循環(huán)的程序，本文證明了當(dāng)循環(huán)展開的次數(shù)足夠大時(shí)，BMPS算法對(duì)于RHS錯(cuò)誤是準(zhǔn)完備的。
　　 本文對(duì)所提BMPS算法進(jìn)行了初步的實(shí)驗(yàn)評(píng)估。本文深入分析了調(diào)試領(lǐng)域權(quán)威標(biāo)準(zhǔn)西門子標(biāo)準(zhǔn)中的TCAS程序，得出TCAS程序的41個(gè)錯(cuò)誤版本中有39個(gè)版本是RHS錯(cuò)誤。本文還對(duì)大量小型錯(cuò)誤C程序進(jìn)行了調(diào)試實(shí)驗(yàn)，實(shí)驗(yàn)結(jié)果表明BMPS能