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

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

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

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