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

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

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

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