【摘要】：軟件系統(tǒng)在未來(lái)的城市建設(shè)中發(fā)揮著非常重要的作用,因此保證其功能正確性是進(jìn)行軟件開發(fā)的關(guān)鍵因素。層次狀態(tài)遷移矩陣(Hierarchical State Transition Matrix,HSTM)是一種流行的軟件設(shè)計(jì)語(yǔ)言,被廣泛應(yīng)用于嵌入式軟件設(shè)計(jì)中。對(duì)于具有復(fù)雜層次結(jié)構(gòu)及調(diào)用關(guān)系的HSTM設(shè)計(jì),其執(zhí)行路徑通常難以跟蹤和調(diào)試,如果HSTM設(shè)計(jì)中的特定變量的首次值變化到其后續(xù)引用的執(zhí)行路徑(稱為更改-引用路徑)能夠自動(dòng)的被輸出,那么這些路徑可以幫助HSTM設(shè)計(jì)者更好的跟蹤變量的變化及使用情況,并分析潛在錯(cuò)誤的成因,從而有利于開發(fā)出功能正確及穩(wěn)定的軟件。目前尚未有針對(duì)HSTM設(shè)計(jì)的更改-引用路徑檢測(cè)算法及工具實(shí)現(xiàn)。本文基于形式驗(yàn)證中的狀態(tài)空間搜索技術(shù),提出了針對(duì)HSTM軟件設(shè)計(jì)中更改-引用路徑的檢測(cè)算法;針對(duì)狀態(tài)空間探索中存在的狀態(tài)空間爆炸問(wèn)題(即狀態(tài)數(shù)目過(guò)多導(dǎo)致探索無(wú)法在有限時(shí)間內(nèi)利用有限計(jì)算資源完成),利用無(wú)狀態(tài)顯式搜索(Stateless Explicit State Exploration,SESE)以及限界上下文切換(Bounded Context Switch,BCS)技術(shù)來(lái)有效緩解狀態(tài)空間爆炸問(wèn)題;此外,在對(duì)更改-引用路徑進(jìn)行檢測(cè)時(shí),需要對(duì)HSTM設(shè)計(jì)進(jìn)行死鎖檢查以及閾值檢查,以避免輸出錯(cuò)誤的檢測(cè)結(jié)果。算法的大致步驟如下:首先對(duì)HSTM設(shè)計(jì)進(jìn)行解析,將其轉(zhuǎn)換成一個(gè)狀態(tài)遷移系統(tǒng);其次將用戶輸入的更改-引用路徑規(guī)約進(jìn)行解析;然后利用顯式狀態(tài)空間搜索技術(shù)對(duì)HSTM對(duì)應(yīng)的狀態(tài)遷移系統(tǒng)進(jìn)行路徑檢測(cè),通過(guò)SESE技術(shù)記憶每個(gè)時(shí)間步的可達(dá)狀態(tài)集,利用BCS技術(shù)限制到達(dá)當(dāng)前狀態(tài)集的進(jìn)程間切換數(shù);如果到達(dá)某個(gè)狀態(tài)時(shí)檢測(cè)到了更改-引用路徑則輸出到達(dá)該狀態(tài)的詳細(xì)轉(zhuǎn)換路徑,否則輸出結(jié)果顯示為無(wú)。本文將提出的更改-引用路徑檢測(cè)算法在課題組前期開發(fā)的Garakabu2形式化模型檢測(cè)工具中進(jìn)行了實(shí)現(xiàn)。除算法本身外,設(shè)計(jì)實(shí)現(xiàn)了更改-引用路徑規(guī)約描述的解析功能,最短更改-引用路徑的輸出功能。實(shí)驗(yàn)結(jié)果表明,本文提出的算法能夠?qū)?fù)雜HSTM軟件設(shè)計(jì)中的更改-引用路徑進(jìn)行有效檢測(cè)及輸出,對(duì)設(shè)計(jì)者開發(fā)出正確的HSTM軟件設(shè)計(jì)可以起到顯著的幫助作用。
【學(xué)位授予單位】：大連理工大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2018
【分類號(hào)】：TP311.52

【參考文獻(xiàn)】

相關(guān)期刊論文 前9條

1 魏歐;石玉峰;徐丙鳳;黃志球;陳哲;;軟件模型檢測(cè)中的抽象模型研究綜述[J];計(jì)算機(jī)研究與發(fā)展;2015年07期

2 金繼偉;馬菲菲;張健;;SMT求解技術(shù)簡(jiǎn)述[J];計(jì)算機(jī)科學(xué)與探索;2015年07期

3 侯剛;周寬久;勇嘉偉;任龍濤;王小龍;;模型檢測(cè)中狀態(tài)爆炸問(wèn)題研究綜述[J];計(jì)算機(jī)科學(xué);2013年S1期

4 孫宏旭;邢薇;陶林;;基于有限狀態(tài)機(jī)的模型轉(zhuǎn)換方法的研究[J];計(jì)算機(jī)技術(shù)與發(fā)展;2012年02期

5 樊曉光;褚文奎;張鳳鳴;;軟件安全性研究綜述[J];計(jì)算機(jī)科學(xué);2011年05期

6 趙艷紅;郭銀章;白尚旺;;基于時(shí)間解耦的分布對(duì)象中間件異步通信消息轉(zhuǎn)換機(jī)制研究[J];計(jì)算機(jī)應(yīng)用與軟件;2008年10期

7 袁志斌;;軟件開發(fā)的形式化方法[J];電腦與電信;2008年07期

8 周修毅;趙建華;李宣東;鄭國(guó)梁;;實(shí)時(shí)系統(tǒng)的模型檢驗(yàn)中針對(duì)共享變量的優(yōu)化技術(shù)[J];計(jì)算機(jī)科學(xué);2005年07期

9 林惠民,張文輝;模型檢測(cè):理論、方法與應(yīng)用[J];電子學(xué)報(bào);2002年S1期

，

本文編號(hào)：2633838