基于上下文定界的并發(fā)程序驗證技術(shù)研究.pdf

1、隨著多核計算的興起，并發(fā)軟件成為計算機輔助驗證的重要目標。并發(fā)軟件系統(tǒng)在社會生活、國民經(jīng)濟等諸多關(guān)鍵領(lǐng)域的應用愈加普遍，軟件系統(tǒng)存在的微小錯誤或漏洞可能會引起重大的經(jīng)濟損失甚至難以預計的后果，檢測軟件缺陷的形式化驗證技術(shù)成為學術(shù)界和工業(yè)界備受關(guān)注的熱點。
　　近年來，大型并發(fā)軟件系統(tǒng)普遍采用任務(wù)驅(qū)動或者事件驅(qū)動的編程方法，本文的研究重點是針對并發(fā)程序的形式化驗證技術(shù)，通過對其抽象模型進行高效的可達性分析，確定抽象模型是否滿足預期的

2、性質(zhì)或者規(guī)格?？蛇_性分析是一種常見的程序驗證技術(shù)，通過搜索程序執(zhí)行產(chǎn)生的狀態(tài)空間，確定程序是否會到達某些錯誤的狀態(tài)，從而查找程序中的錯誤或漏洞。論文針對并發(fā)程序的可達性分析進行研究，取得如下創(chuàng)新成果：
　　1.針對Fork/Join并行模式的并發(fā)程序的可達性問題進行分析，將可以模擬Fork/Join并行線程創(chuàng)建的并發(fā)程序執(zhí)行的抽象模型（動態(tài)并發(fā)下推系統(tǒng)）化簡為對應的并發(fā)下推系統(tǒng)，化簡后的系統(tǒng)可以使用現(xiàn)有的k-定界可達算法進行求解。

3、
　　2.采用上下文定界方法抑制狀態(tài)空間爆炸問題，通過約束系統(tǒng)進程的消息隊列是良序的，證明其上下文切換定界可達性問題是可判定的。提出一種構(gòu)造模擬遞歸隊列并發(fā)程序執(zhí)行的多棧下推系統(tǒng)的轉(zhuǎn)換方法，將其上下文切換定界可達性問題轉(zhuǎn)換為多棧下推系統(tǒng)的階定界可達性問題。
　　3.基于上下文定界思想和良序排隊約束，提出一種針對多棧下推系統(tǒng)的上下文切換定界可達算法，對下推系統(tǒng)迭代地應用標準Post*算法，窮盡地計算k次上下文切換內(nèi)正向可達的格