On-the-Fly和動(dòng)態(tài)的軟件模型檢測(cè)方法研究.pdf

1、隨著軟件規(guī)模不斷擴(kuò)大，內(nèi)部結(jié)構(gòu)愈發(fā)復(fù)雜，應(yīng)用環(huán)境日益開(kāi)放，軟件可信性已成為人們廣泛關(guān)注的熱點(diǎn)。在軟件開(kāi)發(fā)的不同階段，軟件可信性呈現(xiàn)出各種屬性形態(tài)，涵蓋正確性、可靠性、安全性等，它是軟件諸多屬性的綜合體現(xiàn)。如何驗(yàn)證軟件可信性是可信軟件的關(guān)鍵研究領(lǐng)域，采用模型檢測(cè)技術(shù)驗(yàn)證軟件的時(shí)序正確性是其中一個(gè)極其重要的研究方向。軟件模型檢測(cè)是形式化證明軟件是否滿(mǎn)足期望性質(zhì)的算法類(lèi)驗(yàn)證方法，其自動(dòng)化程度高，當(dāng)軟件違反期望性質(zhì)時(shí)還會(huì)給出一個(gè)系統(tǒng)反例。由于系

2、統(tǒng)模型隨變量數(shù)或并發(fā)組件數(shù)等因素的線(xiàn)性增長(zhǎng)呈指數(shù)級(jí)增長(zhǎng)，且軟件模型檢測(cè)窮盡搜索系統(tǒng)模型的狀態(tài)空間以尋找反例，因此模型檢測(cè)可能無(wú)法在期望的時(shí)空開(kāi)銷(xiāo)內(nèi)完成驗(yàn)證，即產(chǎn)生狀態(tài)空間爆炸問(wèn)題。控制狀態(tài)空間爆炸始終是軟件模型檢測(cè)的一個(gè)重大研究方向。
　　狀態(tài)空間爆炸存在于面向系統(tǒng)模型的靜態(tài)模型檢測(cè)，也存在于基于程序執(zhí)行的動(dòng)態(tài)模型檢測(cè)。在LTL（Linear Temporal Logic）靜態(tài)模型檢測(cè)領(lǐng)域，on-the-fly自動(dòng)機(jī)理論的LTL模

3、型檢測(cè)是一種有效緩解狀態(tài)爆炸的方法。它首先將LTL性質(zhì)翻譯成與其否定公式等價(jià)的ω-自動(dòng)機(jī)，然后將LTL模型檢測(cè)問(wèn)題轉(zhuǎn)化成ω-自動(dòng)機(jī)的空性檢測(cè)問(wèn)題，即系統(tǒng)模型和否定性質(zhì)自動(dòng)機(jī)的同步積ω-自動(dòng)機(jī)，并且采用on-the-fly方式空性檢測(cè)，若積自動(dòng)機(jī)非空，該方法無(wú)需建立整個(gè)積空間就能找到反例。通常LTL性質(zhì)翻譯涉及Büchi自動(dòng)機(jī)和廣義Büchi自動(dòng)機(jī)兩種ω-自動(dòng)機(jī)，同時(shí)，空性檢測(cè)方法分為順序和并行兩類(lèi)計(jì)算模式，在這幾類(lèi) on-the-fly

4、空性檢測(cè)方法中仍有許多待研究的重要挑戰(zhàn)。在并發(fā)軟件的動(dòng)態(tài)模型檢測(cè)領(lǐng)域，并發(fā)線(xiàn)程的交織爆炸會(huì)導(dǎo)致執(zhí)行狀態(tài)空間爆炸，有狀態(tài)動(dòng)態(tài)偏序歸約方法能有效縮減交織數(shù)量，但該方法的計(jì)算性能仍有待提高。
　　本文立足軟件模型檢測(cè)方法，重點(diǎn)圍繞on-the-fly自動(dòng)機(jī)理論的LTL模型檢測(cè)中三類(lèi)空性檢測(cè)方法，以及動(dòng)態(tài)模型檢測(cè)中有狀態(tài)動(dòng)態(tài)偏序歸約方法，分別針對(duì)這四種模型檢測(cè)方法存在的具體問(wèn)題，開(kāi)展如下研究，以進(jìn)一步提升模型檢測(cè)方法的性能：
　?。?/p>

5、1）針對(duì)NDFS（Nested Depth-First Search）Büchi自動(dòng)機(jī)空性檢測(cè)返回不必要的長(zhǎng)反例問(wèn)題，其妨礙反例理解且傾向于消耗較多時(shí)空代價(jià)，提出一種 on-the-fly深度有界的Büchi自動(dòng)機(jī)空性檢測(cè)方法。它利用深度有界縮減策略約束NDFS方法，使其遍歷有界積空間。首先深度有界縮減策略設(shè)定積自動(dòng)機(jī)的狀態(tài)最小深度為受限參數(shù)，并增量完備地計(jì)算有界積狀態(tài)集，然后利用NDFS窮盡遍歷on-the-fly生成的有界積空間以尋

6、找反例。實(shí)驗(yàn)結(jié)果表明，該方法普遍適用于積自動(dòng)機(jī)非空的情況，能有效返回較優(yōu)短反例，產(chǎn)生的時(shí)空代價(jià)與同類(lèi)算法相當(dāng)。
　　（2）針對(duì)全面結(jié)合位狀態(tài)哈希的SCC（Strongly Connected Components）廣義Büchi自動(dòng)機(jī)空性檢測(cè)方法對(duì)于 SCC合并的終止條件考慮不全面的問(wèn)題，提出位狀態(tài)哈希終端SCC的on-the-fly廣義Büchi自動(dòng)機(jī)空性檢測(cè)方法。首先形式化給出終端SCC的定義，然后針對(duì)完全遍歷的終端 SCC采

7、用位狀態(tài)哈希技術(shù)。理論證明了方法的正確性，而且實(shí)驗(yàn)結(jié)果表明該方法覆蓋了SCC合并終止的所有情況，縮減了空性檢測(cè)的內(nèi)存消耗。在此方法基礎(chǔ)上，再融入復(fù)合啟發(fā)式策略，提出位狀態(tài)哈希終端SCC的on-the-fly啟發(fā)式廣義Büchi自動(dòng)機(jī)空性檢測(cè)方法。復(fù)合啟發(fā)式將每個(gè)狀態(tài)的所有后繼遷移分成四個(gè)等級(jí)，每次優(yōu)先選擇最高等級(jí)的一個(gè)遷移執(zhí)行積空間遍歷。實(shí)驗(yàn)結(jié)果表明，該方法進(jìn)一步提高了廣義Büchi自動(dòng)機(jī)空性檢測(cè)的時(shí)空性能，相比同類(lèi)算法，其性能更優(yōu)。<

8、br>　　（3）針對(duì)一種結(jié)合最大接受前驅(qū)的on-the-fly并行空性檢測(cè)方法，其面對(duì)傳播的接受環(huán)最大接受前驅(qū)處于環(huán)外的情境，無(wú)法通過(guò)傳播接受前驅(qū)識(shí)別接受環(huán)的問(wèn)題。提出一種傳播最大和最新接受前驅(qū)的on-the-fly并行空性檢測(cè)方法。在首次遍歷積自動(dòng)機(jī)圖時(shí)，它采用最大接受前驅(qū)和最新接受前驅(qū)的雙值傳播模式，最大接受前驅(qū)仍保留原方法的傳播特征，引入的最新接受前驅(qū)追蹤并行空性檢測(cè)的局部遍歷特征。大量實(shí)驗(yàn)結(jié)果表明，在顯現(xiàn) on-the-fly優(yōu)

9、勢(shì)的提前終止率方面，所提方法高于原始方法，因此在原始方法on-the-fly識(shí)別失效時(shí)該方法仍能成功識(shí)別接受環(huán)，且該方法提高了并行空性檢測(cè)的時(shí)空性能。
　?。?）無(wú)狀態(tài)或有狀態(tài)的動(dòng)態(tài)偏序歸約方法在驗(yàn)證多線(xiàn)程并發(fā)程序時(shí)，候選回溯集的計(jì)算是更新回溯集的關(guān)鍵步驟之一，實(shí)際上原始候選回溯集的計(jì)算成本超出了回溯集的更新需求。針對(duì)上述問(wèn)題，提出收縮候選回溯集的有狀態(tài)動(dòng)態(tài)偏序歸約方法。設(shè)收縮候選回溯條件二為回溯點(diǎn)后首個(gè)與待執(zhí)行遷移存在發(fā)生先序關(guān)