Java多線程程序中存在并發(fā)、同步和交互行為,導(dǎo)致狀態(tài)爆炸,算法錯(cuò)誤檢測(cè)難度較大。調(diào)試方法和測(cè)試方法都難以覆蓋并發(fā)程序全部執(zhí)行路徑;軟件模型檢測(cè)方法自動(dòng)搜索并發(fā)程序全部執(zhí)行路徑,但在狀態(tài)爆炸時(shí)難以完成。本文針對(duì)Java多線程程序提出層次著色Petri網(wǎng)（Hierarchical Coloured Petri Net,HCPN）粗粒度自動(dòng)建模方法,在不影響模型檢測(cè)結(jié)果的前提下,實(shí)現(xiàn)了模型及其狀態(tài)空間規(guī)�？s減,有利于模型檢測(cè)效率的提升。工作如下:1.提出了屬性公式處理策略。粗粒度模型必須保留屬性公式中待檢測(cè)的狀態(tài)信息,待檢測(cè)狀態(tài)相關(guān)的源程序語句須采用細(xì)粒度描述。因此本文提出了包含關(guān)鍵變量注釋方法、檢測(cè)相關(guān)語句自動(dòng)識(shí)別方法、相關(guān)模型片段提示方法的屬性公式處理策略。2.提出了包含語句粗細(xì)粒度判定功能的程序預(yù)處理方法。以語句為單位讀取源程序,為每個(gè)函數(shù)構(gòu)建語句二叉樹,依據(jù)本文提出的粒度判定策略實(shí)現(xiàn)源程序語句粒度判定并標(biāo)注。3.提出了細(xì)粒度和粗粒度模型描述方法。源程序中函數(shù)映射為模型頁面,語句則根據(jù)類型分別映射為不同的模型片段。針對(duì)并發(fā)、同步、交互、檢測(cè)相關(guān)語句等特定語句,采用細(xì)粒度描述,將一條語... 

【文章來源】：內(nèi)蒙古大學(xué)內(nèi)蒙古自治區(qū)211工程院校

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

【學(xué)位級(jí)別】：碩士

【部分圖文】：

類表結(jié)構(gòu)

內(nèi)蒙古大學(xué)碩士學(xué)位論文圖 3.6(a)中的代碼段除括號(hào)、變量注釋外共包括 6 條語句，分別按序號(hào)對(duì)應(yīng)圖 3.6(b)中語句二叉樹中的 6 個(gè)結(jié)點(diǎn)，該代碼段的 if_else 結(jié)構(gòu)中分別嵌套兩個(gè)順序結(jié)構(gòu)。語句 2 與語句 1之間為嵌套關(guān)系，語句 2 與語句 3 之間為順序關(guān)系，因此結(jié)點(diǎn) 2 作為結(jié)點(diǎn) 1 的左子結(jié)點(diǎn)，結(jié)點(diǎn)3 作為結(jié)點(diǎn) 2 的右子結(jié)點(diǎn)。語句 1 與語句 4 為順序關(guān)系，因此結(jié)點(diǎn) 4 作為結(jié)點(diǎn) 1 的右子結(jié)點(diǎn)，語句 4、5、6 同理。語句 1 為 if 語句，對(duì)應(yīng)結(jié)點(diǎn) 1 的 Type 屬性為 if，語句 4 為 else 語句，對(duì)應(yīng)結(jié)點(diǎn) 4 的 Type 屬性為 else；語句 2、3、5、6 均為賦值語句，因此對(duì)應(yīng)結(jié)點(diǎn) 2、3、4、5 的Type 屬性值為 assignment。

VarList結(jié)構(gòu)

【參考文獻(xiàn)】：
期刊論文
[1]一種面向CPS的控制應(yīng)用程序協(xié)同驗(yàn)證方法[J]. 張雨,董云衛(wèi),馮文龍,黃夢(mèng)醒.  軟件學(xué)報(bào). 2017(05)
[2]基于CEGAR的C程序空指針解引用檢測(cè)[J]. 段釗,田聰,段振華.  計(jì)算機(jī)研究與發(fā)展. 2016(01)
[3]軟件模型檢測(cè)中的抽象模型研究綜述[J]. 魏歐,石玉峰,徐丙鳳,黃志球,陳哲.  計(jì)算機(jī)研究與發(fā)展. 2015(07)
[4]基于CEGAR的Web應(yīng)用驗(yàn)證[J]. 高洪皓,繆淮扣,曾紅衛(wèi).  計(jì)算機(jī)學(xué)報(bào). 2014(04)
[5]基于SMT求解器的路徑敏感程序驗(yàn)證[J]. 何炎祥,吳偉,陳勇,徐超.  軟件學(xué)報(bào). 2012(10)
[6]程序代碼中隱含數(shù)據(jù)與控制的Petri網(wǎng)建模技術(shù)[J]. 周國富,杜卓敏.  軟件學(xué)報(bào). 2011(12)
[7]一種基于認(rèn)知模型檢測(cè)的Web服務(wù)組合驗(yàn)證方法[J]. 駱翔宇,譚征,蘇開樂,吳立軍.  計(jì)算機(jī)學(xué)報(bào). 2011(06)
[8]面向源代碼的軟件模型檢測(cè)及其實(shí)現(xiàn)[J]. 何愷鐸,顧明,宋曉宇,李力,李江.  計(jì)算機(jī)科學(xué). 2009(01)
[9]基于抽象-驗(yàn)證-細(xì)化范例的軟件模型檢測(cè)[J]. 劉吉鋒,孫吉貴.  計(jì)算機(jī)科學(xué). 2006(12)
[10]軟件模型檢測(cè)中的抽象[J]. 袁志斌,徐正權(quán),王能超.  計(jì)算機(jī)科學(xué). 2006(07)

碩士論文
[1]基于LTL的并行軟件系統(tǒng)CPN模型啟發(fā)式模型檢測(cè)方法研究[D]. 任海芬.內(nèi)蒙古大學(xué) 2018
[2]單函數(shù)Java程序到CPN模型轉(zhuǎn)換工具的設(shè)計(jì)與實(shí)現(xiàn)[D]. 霍明倩.內(nèi)蒙古大學(xué) 2018
[3]FPGA程序的形式化建模與分析方法研究[D]. 陳瓏.華僑大學(xué) 2015
[4]模型檢測(cè)在軟件方面的應(yīng)用[D]. 黎吾平.吉林大學(xué) 2008



本文編號(hào)：3625643