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

【參考文獻(xiàn)】

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

1 單來(lái)成;吳明花;;淺析模型檢測(cè)技術(shù)[J];信息技術(shù)與信息化;2014年07期

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

3 朱維軍;周清雷;張海賓;;從線性時(shí)序邏輯公式到自動(dòng)機(jī)的轉(zhuǎn)換算法(英文)[J];中國(guó)通信;2012年06期

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

5 彭曉紅;劉久富;;基于模型檢測(cè)的軟件測(cè)試技術(shù)[J];軟件導(dǎo)刊;2009年03期

6 殷澇，

本文編號(hào)：2711181