3.1.3　基于有限狀態(tài)機(jī)和時間自動機(jī)模型

狀態(tài)機(jī)是描述系統(tǒng)狀態(tài)與狀態(tài)轉(zhuǎn)換的一種形式化方法，通常由狀態(tài)、轉(zhuǎn)換、事件、活動和動作等部分組成，利用狀態(tài)機(jī)可以精確地描述對象的行為。在計算機(jī)科學(xué)中，狀態(tài)機(jī)的使用非常普遍，尤其是在通信協(xié)議及嵌入式軟件的建模及驗證領(lǐng)域。

由于實時嵌入式軟件大多基于狀態(tài)，而有限狀態(tài)機(jī)（FSM）模型用觸發(fā)事件和狀態(tài)遷移描述系統(tǒng)的行為，因此適用于一般實時嵌入式軟件的開發(fā)和測試的形式化描述。此外，為了增強(qiáng)有限狀態(tài)機(jī)的描述能力，簡化描述，使各狀態(tài)之間的變化清晰化，最終提高對局部以致整個模型的描述與分析能力，出現(xiàn)了眾多基于有限狀態(tài)機(jī)的擴(kuò)展方法，如CFSM（Communicating FSM）、EFSM（Extended FSM）、CEFSM（Communicating EFSM）、PFSM（Probability FSM）等。此外，基于FSM的時間自動機(jī)（Timed Automata，TA）也取得了較多的研究成果。

基于有限狀態(tài)機(jī)的測試模型假設(shè)軟件在某個時刻總是處于某個狀態(tài)，并且當(dāng)前狀態(tài)決定了軟件可能的輸入，而且從該狀態(tài)向其他狀態(tài)的遷移取決于當(dāng)前的輸入。有限狀態(tài)機(jī)模型適用于把測試數(shù)據(jù)表達(dá)為輸入序列的測試方法，并可以利用圖的遍歷算法自動生成測試序列。

有限狀態(tài)機(jī)可以用狀態(tài)遷移圖或狀態(tài)遷移矩陣表示，可以根據(jù)狀態(tài)覆蓋或遷移覆蓋生成測試用例。有限狀態(tài)機(jī)模型有成熟的理論基礎(chǔ)，并且可以利用形式化語言和自動機(jī)理論來設(shè)計、操縱和分析，適合描述反應(yīng)式系統(tǒng)。早期基于FSM的經(jīng)典軟件測試方法包括T方法、U方法、D方法和W方法等。隨著FSM技術(shù)的不斷發(fā)展，逐漸出現(xiàn)了基于擴(kuò)展的有限狀態(tài)機(jī)的測試方法，如基于EFSM的測試輸入數(shù)據(jù)自動選取方法，該方法通過區(qū)間削減和分段梯度最優(yōu)下降算法自動選取測試輸入所需的測試數(shù)據(jù)，從而代替手工選取測試數(shù)據(jù)的工作，提高測試效率，大大降低軟件測試過程中的花費。EFSM比FSM能夠更加精確地刻畫軟件系統(tǒng)的行為，但由于擴(kuò)展有限狀態(tài)機(jī)中的遷移存在前置條件，單純地將基于有限狀態(tài)機(jī)的測試方法用于擴(kuò)展有限狀態(tài)機(jī)會產(chǎn)生很多問題，如測試序列不可執(zhí)行、存在不確定性等問題。

TA是在傳統(tǒng)FSM基礎(chǔ)上為遷移添加時鐘約束，為狀態(tài)添加不變式約束而得到的，添加到遷移上的時鐘約束表示只有在此約束被滿足時遷移才被激活，而添加到狀態(tài)上的不變式約束表示只有在此不變式被滿足時系統(tǒng)才能停留在此狀態(tài)。一種基于時間自動機(jī)的實時系統(tǒng)測試方法如下：將時間安全輸入/輸出自動機(jī)描述的系統(tǒng)模型轉(zhuǎn)換為不含抽象時間延遲遷移的穩(wěn)定符號狀態(tài)遷移圖，然后采用基于標(biāo)號遷移系統(tǒng)的測試方法來靜態(tài)生成滿足各種結(jié)構(gòu)覆蓋標(biāo)準(zhǔn)的遷移動作序列。最后，給出根據(jù)遷移動作序列構(gòu)造和執(zhí)行測試用例的過程，該過程引入了時間延遲變量目標(biāo)函數(shù)，并采用線性約束求解方法動態(tài)求解遷移動作序列中的時間延遲變量。