【摘要】：在軟件生命周期中,軟件測試是保證軟件質(zhì)量的重要環(huán)節(jié)之一。軟件測試可分為動態(tài)檢測和靜態(tài)檢測,動態(tài)檢測是通過測試用例在運行時檢測正確性,靜態(tài)檢測則是直接分析源代碼。靜態(tài)檢測技術通過強大的抽象解釋使分析精確而高效,并且擁有自動化、完善性(完全控制和數(shù)據(jù)覆蓋)等特點,使其在工業(yè)環(huán)境中成為一種廣受歡迎的方法。但隨著計算機技術的發(fā)展,并發(fā)軟件已經(jīng)有了廣泛的應用。并發(fā)軟件的發(fā)展給軟件測試帶來了新的挑戰(zhàn),執(zhí)行路徑的不確定性是并發(fā)軟件的重要特性,也是測試的難點所在,由于并發(fā)狀態(tài)空間較大,直接將順序程序的靜態(tài)檢測技術應用于交錯執(zhí)行的并發(fā)程序中效果并不好。線程模塊化分析方法不用考慮線程交織以及相關的執(zhí)行構(gòu)建說明,可以通過分別分析每個線程來實現(xiàn)對并發(fā)程序的驗證。線程模塊化分析方法的主要優(yōu)勢在于可以用最小的代價將順序抽象解釋器提升為并發(fā)抽象解釋器。該方法的核心思想分做兩個步驟:首先,創(chuàng)建線程,并將所有的線程作為一個獨立的順序程序進行分析,同時收集其他線程對其變量的影響。然后,重新分析所有的線程,并且計算線程間的干涉,保存發(fā)現(xiàn)的新的行為和新的可能的干涉。遞歸這個過程直到干涉穩(wěn)定。但傳統(tǒng)的線程模塊化分析方法是基于線程交互的非關系型流不敏感的具體語義,分析更容易處理但結(jié)果不是很準確,本文在線程模塊化分析方法的基礎上實現(xiàn)了線程間的流敏感并提出了一種基于數(shù)據(jù)流圖的約束,使分析結(jié)果更加準確。本文主要創(chuàng)新點如下:1.在原始模塊化分析方法的基礎上,我們提出了一種基于抽象解釋的流敏感的線程模塊化分析方法,使分析更加準確。2.我們開發(fā)了一種輕量級的基于數(shù)據(jù)流圖的約束框架,用于檢測線程內(nèi)的干涉是否有效,以提高分析效率,提升分析精度。3.在上述理論研究支持下,我們基于這種算法開發(fā)了一個面向嵌入式并發(fā)程序的分析工具原型。4.以驗證航空發(fā)動機控制系統(tǒng)為例,通過應用我們的線程模塊化分析方法對系統(tǒng)進行了靜態(tài)檢測,展示了算法對嵌入式并發(fā)程序分析與驗證的能力。
【學位授予單位】：華東師范大學
【學位級別】：碩士
【學位授予年份】：2018
【分類號】：TP311.53
【圖文】：

y) 中是否存在除零錯誤。1. 根據(jù) x,y 的值建 個坐標系， 來表 所有 x 和 y 可能的取值范圍，如圖2.2在第 象限的斜線表 a = b 的情況，即可能會出現(xiàn)除零的集合。2. 如何判斷變量 a,b 會同時取到斜線上的值，最簡單粗暴的 式是進 枚舉，檢查所有 a,b 可能的取值，看是否同時在這條斜線上，這是 種普通測試的做法。隨著變量的增多，這種 法的 作量的增長是指數(shù)級的，所以不可能枚舉出所有的可能值。利 抽象解釋，我們可以根據(jù)規(guī)則對程序進

圖 2.2: 建 坐標系圖 2.3: 矩陣取值法 例利 區(qū)間分析的 法，得到變量的最 值和最 值，如圖2.3，在 維坐標系中畫 個矩形，矩形框內(nèi)的值是變量 x,y 所有可能的取值， xi, xa, yi, ya來分別表 x,y 的最 值和最 值。然后我們通過對矩形集合和斜線集合做交運算，如果運算結(jié)果為空，則說明不存在除零的可能，如果交集不為空，則說明有除零的可能。3. 上 的 法雖然可以解決問題，但效率很低，因為利 x 和 y 畫出的矩形抽象的太粗糙， 包含很多 x,y 不可能的賦值

抽象的太粗糙， 包含很多 x,y 不可能的賦值，我們可以繼續(xù)優(yōu)化，將按照規(guī)則，將矩形細化，建 多個精確的多邊形，其中利 變量 x,y 在程序中的關系，并且根據(jù)控制流圖和結(jié)構(gòu)流圖，我們可以畫出如圖2.4所 。10

【參考文獻】

相關期刊論文 前1條

1 劉樹錕;陽小華;;程序不變量檢測技術[J];計算機工程與科學;2011年03期

本文編號：2786067