隨著POSIX多線程（POSIX Threads,Pthreads）廣泛應用于各類復雜并發(fā)系統(tǒng),由線程競爭資源或推進順序不合適所引發(fā)的死鎖問題變得越來越常見。死鎖會造成多線程程序崩潰或非正常終止,對于安全性要求較高的行業(yè)會帶來災難性的后果,因此如何有效檢測出POSIX多線程程序中潛在的死鎖至關重要。近年來,主流的死鎖檢測方法主要有形式化模型靜態(tài)死鎖檢測分析和動態(tài)死鎖檢測兩種。相比動態(tài)死鎖檢測方法而言,基于形式化模型分析的靜態(tài)死鎖檢測方法由于具備完善的數(shù)學理論并且可以在軟件系統(tǒng)編譯之前檢測到程序中潛在的死鎖,因此備受廣大學者推崇。但是該方法仍存在以下幾方面問題需要研究:（1）形式化語言和多線程程序語義描述存在很大偏差,不能直接實現(xiàn)多線程程序語義到形式化模型的映射;（2）使用形式化語言對多線程程序建模時,很容易造成模型過于龐大,以至于在模型檢測階段會產(chǎn)生狀態(tài)空間爆炸;（3）難以對多線程程序指針建立等價語義的形式化模型。針對以上問題,本文基于擴展CSP（extended CSP,CSP#）提出了一種對POSIX多線程程序自動建模與死鎖檢測的新方法,主要從以下幾方面開展研究:一、提出一種POS... 

【文章來源】：太原理工大學山西省 211工程院校

【文章頁數(shù)】：76 頁

【學位級別】：碩士

【部分圖文】：

模型檢測基本流程

POSIX多線程程序轉換為CSP#模型流程

圖 3-3 共享內(nèi)存數(shù)據(jù)讀寫方式 mode of shared memory data readiP 中聲明如式(3-1)所示：sp::Chanouttypename_osp::Chanintypename_in

【參考文獻】：
期刊論文
[1]面向資源的物聯(lián)網(wǎng)系統(tǒng)形式化建模與驗證[J]. 馬莉,李維康,梁晨,李愛萍.  小型微型計算機系統(tǒng). 2018(01)
[2]使用鎖分配圖動態(tài)檢測混合死鎖[J]. 禹振,蘇小紅,邱景.  計算機研究與發(fā)展. 2017(07)
[3]由MDA/PIM到Java代碼的轉換及驗證[J]. 李凱寧,武淑紅,王耀力.  計算機工程與設計. 2017(06)
[4]模型檢測在完整性形式化驗證中的應用研究[J]. 嚴亞偉,周雁舟,惠文濤.  計算機工程與應用. 2017(04)
[5]多核多線程技術綜述[J]. 眭俊華,劉慧娜,王建鑫,秦慶旺.  計算機應用. 2013(S1)
[6]基于Elastos線程同步機制的死鎖檢測技術研究[J]. 張捷,陳榕.  計算機科學. 2008(12)
[7]通信系統(tǒng)演算CCS與自動驗證工具MWB[J]. 李元,李祥.  通信技術. 2005(S1)
[8]基于Petri網(wǎng)的模型檢測研究[J]. 蔣屹新,林闖,曲揚,尹浩.  軟件學報. 2004(09)
[9]形式化方法B及其程序規(guī)約機理[J]. 肖美華,薛錦云.  計算機工程. 2004(16)
[10]B語言和方法與Z、VDM的比較[J]. 鄒盛榮,鄭國梁.  計算機科學. 2002(10)

碩士論文
[1]基于Petri網(wǎng)的多線程死鎖檢測研究[D]. 黃理.中國科學技術大學 2015



本文編號：3493603