發(fā)布時間：2020-04-19 23:07

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

【參考文獻】

相關期刊論文 前9條

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

2 金繼偉;馬菲菲;張健;;SMT求解技術簡述[J];計算機科學與探索;2015年07期

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

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

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

6 趙艷紅;郭銀章;白尚旺;;基于時間解耦的分布對象中間件異步通信消息轉換機制研究[J];計算機應用與軟件;2008年10期

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

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

9 林惠民,張文輝;模型檢測:理論、方法與應用[J];電子學報;2002年S1期

，

本文編號：2633838