基于時間動態(tài)下推網(wǎng)絡(luò)可達(dá)性分析.pdf

1、隨著多核處理器的發(fā)展，對并發(fā)程序的研究已成為程序設(shè)計的熱點。然而，并發(fā)程序的交錯執(zhí)行存在不確定性，這導(dǎo)致了傳統(tǒng)的測試、仿真、演繹推理技術(shù)很難發(fā)現(xiàn)程序中隱匿的錯誤和漏洞。模型檢測是一種通過窮盡搜索的自動化驗證技術(shù)，作為傳統(tǒng)驗證方法的一種補(bǔ)充，已成為保證程序安全和可靠的重要手段?？蛇_(dá)性分析是一種常用的程序驗證技術(shù)，通過分析程序某一狀態(tài)是否可達(dá)，從而查找程序中的漏洞或錯誤。
　　基于共享內(nèi)存進(jìn)行異步通信是并發(fā)程序中常用的通信方式之一，然

2、而現(xiàn)有模型對該類程序進(jìn)行建模時，其可達(dá)性是不可判定的，基于k-限界技術(shù)可使其為可判定。本文結(jié)合k-限界技術(shù)，對基于共享內(nèi)存進(jìn)行異步通信的并發(fā)程序的可達(dá)性進(jìn)行研究。主要工作如下：
　　針對含有遞歸、動態(tài)線程創(chuàng)建的并發(fā)系統(tǒng)的可達(dá)性分析問題，提出動態(tài)下推網(wǎng)絡(luò)模型DPN，采用k-限界技術(shù)算法實現(xiàn)可達(dá)性分析。由于該算法存在狀態(tài)空間爆炸問題，對模型中下推系統(tǒng)進(jìn)行符號化，縮減狀態(tài)空間，避免窮盡搜索每一條路徑，以便節(jié)省大量計算時間。
　　針

3、對含有遞歸、動態(tài)線程創(chuàng)建的實時并發(fā)系統(tǒng)，提出了時間動態(tài)下推網(wǎng)絡(luò)對其進(jìn)行建模。首先在動態(tài)下推網(wǎng)絡(luò)中引入描述連續(xù)時間的全局時鐘，以及能描述與時間相關(guān)的全局變量和棧字符“年齡”的實數(shù)時鐘。然后給出一種基于時鐘關(guān)鍵點的優(yōu)化技術(shù)來縮減時鐘區(qū)間，緩解轉(zhuǎn)換后的狀態(tài)空間爆炸問題，為了進(jìn)一步縮減狀態(tài)空間，采用僅關(guān)注棧頂?shù)膭討B(tài)轉(zhuǎn)換方法，將連續(xù)的時間動態(tài)下推網(wǎng)絡(luò)轉(zhuǎn)換成時間域表示的動態(tài)下推網(wǎng)絡(luò)，同時給出轉(zhuǎn)換的等價算法，并且證明狀態(tài)p在時間動態(tài)下推網(wǎng)絡(luò)中可達(dá)當(dāng)且