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

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

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

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

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

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

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

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

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

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