Testing vs. Model Checking

??那么JPF所做的是測(cè)試我們的程序是否存在缺陷？不，它通常做得更多，至少當(dāng)用作模型檢查器時(shí)。那么，測(cè)試與模型檢查有什么不同？

??軟件測(cè)試是一組經(jīng)驗(yàn)技術(shù)，您可以在程序中執(zhí)行大量輸入，以確定其行為是否正確。這包括兩個(gè)部分，它們涉及到正確的選擇：test input and test oracle。

states-testing.png

??Testing 測(cè)試技術(shù)在我們?nèi)绾芜x擇輸入時(shí)有所不同(random, "interesting" problem domain values like corner cases etc)，以及對(duì)于被測(cè)系統(tǒng)的了解情況（system under test SUT），以及它的執(zhí)行環(huán)境（黑/灰/白盒），這尤其影響我們?nèi)绾味x和檢查正確的行為。這需要大量的猜測(cè)，或者像Edsger dijkstra所說(shuō)的：“程序測(cè)試最多只能顯示錯(cuò)誤的存在，但絕不能顯示錯(cuò)誤的缺失”，為此，我們通常通過(guò)執(zhí)行“足夠多”的測(cè)試用例來(lái)實(shí)現(xiàn)這一點(diǎn)。測(cè)試復(fù)雜系統(tǒng)通?？梢哉f(shuō)是大海撈針。如果你是一個(gè)優(yōu)秀的測(cè)試人員，你做出了正確的猜測(cè)，并擊中不可避免的缺陷。如果不是，不要擔(dān)心-你的用戶稍后會(huì)發(fā)現(xiàn)它。

states-mc.png

??Model Checking 模型檢驗(yàn)作為一種非形式化方法，不依賴于猜測(cè)。至少理論上是這樣的，如果有違反給定規(guī)范的行為,模型檢查會(huì)找到的。模型檢驗(yàn)被認(rèn)為是一種嚴(yán)格的方法，它詳盡地探索了SUT所有可能的行為。

??為了說(shuō)明這一點(diǎn),請(qǐng)看例子Random number example 這顯示了如果我們有一個(gè)使用隨機(jī)值序列的程序，測(cè)試與模型檢查是不同的:測(cè)試每次只處理一組值,而且我們對(duì)每一組沒(méi)有控制權(quán)。而模型檢查在檢查所有數(shù)據(jù)組合或發(fā)現(xiàn)錯(cuò)誤之前是不會(huì)停止的。

??用Random number example這個(gè)例子，我們至少可以看到程序中的選擇。假設(shè)這是一個(gè)并發(fā)編程示例concurrent programming example，您知道操作系統(tǒng)在線程之間切換的位置嗎？我們所知道的是不同的調(diào)度序列可能導(dǎo)致不同的程序行為（如過(guò)有數(shù)據(jù)競(jìng)爭(zhēng)的話）。但是我們?cè)跍y(cè)試中很難強(qiáng)制改變調(diào)度的行為。有程序/測(cè)試規(guī)格的組合，是“不可測(cè)”。但是作為一臺(tái)虛擬機(jī)，我們的軟件模型檢查器不會(huì)遭受相同的命運(yùn)-它完全控制我們程序的所有線程，而且可以執(zhí)行所有的調(diào)度組合。

??這只是理論，實(shí)際上，“all possible”可能是一個(gè)相當(dāng)大的數(shù)字-對(duì)于現(xiàn)有的計(jì)算資源或我們的耐心來(lái)說(shuō)太大了。假設(shè)一個(gè)程序不同的調(diào)度序列有N個(gè)線程組成（P1...Pn），每個(gè)都有n_i原子指令序列。

interleavings.png

??對(duì)于擁有2個(gè)原子片段的兩個(gè)線程來(lái)說(shuō)，每一個(gè)都給了我們6種不同的調(diào)度組合。對(duì)于有8個(gè)原子片段來(lái)說(shuō)，這個(gè)數(shù)字是12870，有16個(gè)片段的是601080390-這就是為什么它容易產(chǎn)生狀態(tài)爆炸。軟件模型檢查具有可測(cè)量性問(wèn)題，甚至比硬件的模型檢查更重要，因?yàn)槌绦蛲ǔＳ懈嗟臓顟B(tài)。

??There are several things we can do. First, we can optimize the model checker, which is simply an engineering feat. Next, we can find program states which are equivalent with respect to the properties we are checking, which can be done with various degrees of abstractions and value representations. Last, we can try to get to the defect first, before we run out of time or memory. But this is where the boundary between testing and model checking becomes blurred, as it involves things like heuristics about interesting input values or system behaviors, and these heuristics tend to drop reachable program states.

??我們可以做這樣幾件事。首先，我們可以優(yōu)化模型檢查器，這將是一個(gè)工程壯舉。接下來(lái)，我們可以找到與我們正在檢查的屬性等價(jià)的程序狀態(tài)，可以用不同程度的抽象和價(jià)值表示來(lái)完成。最后，我們可以嘗試在再耗盡時(shí)間或內(nèi)存之前先找到缺陷。但是這就是測(cè)試和模型檢查之間的界限變得模糊的地方，因?yàn)樗婕暗街T如關(guān)于有趣的輸入值或系統(tǒng)行為的啟發(fā)式方法，而這些啟發(fā)式方法傾向于刪除可訪問(wèn)的程序狀態(tài)。

??JPF做了這些來(lái)限制狀態(tài)爆炸的發(fā)生。而且大多數(shù)東西都是配置的，而不是硬連接的。所以你不依賴于內(nèi)置的啟發(fā)式方法。但不管我們縮小了多少狀態(tài)空間，與常規(guī)測(cè)試相比，JPF仍然可以觀察到更多關(guān)于程序執(zhí)行的信息，而且它仍然知道執(zhí)行的歷史，以防我們發(fā)現(xiàn)一個(gè)缺陷--這只是第一部分。我們還需要理解它，使它最終可以被解決。