【摘要】：列控系統(tǒng)需求文檔結構的日益復雜,使得傳統(tǒng)的文檔測試方法在問題發(fā)現(xiàn)和測試效率方面逐漸難以滿足要求。模型檢測是一種用于對有窮并發(fā)系統(tǒng)進行正確性檢驗的形式化驗證技術,它是提高系統(tǒng)可靠性的有效手段。本文針對傳統(tǒng)的需求文檔測試方法存在的不足,將模型檢測與軟件測試相結合,在對文檔進行形式化建模驗證的基礎上,利用結果得到的反例生成文檔測試項,提高了文檔測試的自動化水平。狀態(tài)遷移矩陣(State Transition Matrix)的規(guī)模會隨著系統(tǒng)復雜度的提高呈指數(shù)級增長。針對這個問題,本文將分層結構引入狀態(tài)遷移矩陣,使其具有更強的表達能力,以便更加有效的對現(xiàn)實中復雜的軟硬件系統(tǒng)進行建模。首先,對列車制動控制系統(tǒng)需求文檔進行形式化建模,其中分別對緊急制動和常用制動兩個主要模塊進行了層次化建模,以有效緩解隨狀態(tài)和事件數(shù)增加而造成的狀態(tài)空間爆炸問題�；跀U展的建模方法,提出系統(tǒng)建模后的符號化編碼和性質描述規(guī)則,并基于有界模型檢測技術(Bound Model Checking,BMC)進行規(guī)范驗證。通過在實際項目中對復雜軟件文檔的建模測試證明了該方法的可靠性。待驗證性質的LTL公式規(guī)模是影響B(tài)MC轉換公式規(guī)模的關鍵因素,本文首先利用LTL公式的等價性對性質公式進行簡化,其次依據(jù)LTL公式向自動機的轉換方法進行狀態(tài)壓縮,同時利用自動機中狀態(tài)的等價性及可達性,再次壓縮自動機規(guī)模,以達到緩解空間爆炸問題的目的。在此基礎上,利用Garakabu II求解器對模型和屬性進行形式化驗證,將模型檢測得到的反例作為測試需求文檔的用例,以有效減少文檔測試項的設計工作量。
【學位授予單位】：大連理工大學
【學位級別】：碩士
【學位授予年份】：2018
【分類號】：TP311.53

【參考文獻】

相關期刊論文 前10條

1 單來成;吳明花;;淺析模型檢測技術[J];信息技術與信息化;2014年07期

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

3 朱維軍;周清雷;張海賓;;從線性時序邏輯公式到自動機的轉換算法(英文)[J];中國通信;2012年06期

4 楊晉吉;蘇開樂;駱翔宇;林瀚;肖茵茵;;有界模型檢測的優(yōu)化[J];軟件學報;2009年08期

5 彭曉紅;劉久富;;基于模型檢測的軟件測試技術[J];軟件導刊;2009年03期

6 殷澇，

本文編號：2711181