3.2　嵌入式軟件形式化測試技術

3.2.1　基本概念

1.狀態機

狀態機是描述系統狀態與狀態轉換的一種形式化方法，是計算機科學的理論基礎，也是一種強大的建模方法。在計算機科學中，狀態機的使用非常普遍，尤其是在通信協議及實時嵌入式軟件的建模及驗證領域。

通常來說，一個系統的行為可以歸為以下三種類型：

·簡單行為：對于特定輸入，系統總是確切地以同一種方式做出響應，與系統歷史無關。

·連續行為：系統的當前狀態依賴于歷史，而且無法標識一個單獨的狀態。

·基于狀態的行為：系統的當前狀態依賴于歷史，并且能夠與其他系統狀態清晰地區別開。

由于實時嵌入式軟件大多基于狀態，而有限狀態機模型用觸發事件和狀態遷移描述系統的行為，因此適用于一般實時嵌入式軟件的開發和測試的形式化描述。

傳統的狀態機是展示狀態與狀態轉換的圖，由狀態、轉換、事件、活動和動作5個部分組成：

·狀態：表示一個模型在其生存期內的狀況，如滿足某些條件、執行某些操作或等待某些事件。一個狀態的生存期是有限的時間段。

·轉換：表示兩個不同狀態之間的聯系，事件可以觸發狀態之間的轉換。

·事件：在某個時間產生，可以觸發狀態轉換，如信號、對象的創建和銷毀以及超時和條件的改變等。

·活動：在狀態機中進行的一個非原子的執行，由一系列動作組成。

·動作：一個可執行的原子計算，導致狀態的變更或返回一個值。

利用狀態機可以精確地描述對象的行為：從對象的初始狀態起，開始響應事件并執行某些動作，這些事件引起狀態的轉換，對象在新的狀態下又開始響應狀態和執行動作，如此連續進行直到終結。在計算機科學中，狀態機的使用非常普遍：在編譯技術中，通常用有限狀態機描述詞法分析過程；在操作系統進程調度中，通常用狀態機描述進程各個狀態之間的轉化關系；在面向對象分析與設計中，對象的狀態、狀態的轉換、觸發狀態轉換的事件、對象對事件的響應都可以用狀態機來描述。

2.有限狀態機

有限狀態機（FSM）是狀態機的一種，有限狀態機模型是形式化模型的一種。一個有限狀態機可以表示為一個六元組(S,S₀,δ,λ,I,O)：

·S：有限狀態的集合。

·S₀：狀態中的一種，是所有狀態的初態。

·δ：狀態轉換函數。

·λ：輸出函數。

·I：有限輸入字符集。

·O：有限輸出字符集。

按照FSM的性質，可具體劃分如下：

·完全（Complete）有限狀態機：對于一個FSM，如果對每一個狀態和每一個輸入，δ和λ都有定義，那么稱為完全FSM，否則稱為不完全（Incomplete）FSM。

·可重置（Reset Capacity）有限狀態機：對于一個FSM，如果存在一個輸入，對于任何一個狀態，都能使該FSM轉換至初始狀態，則該FSM具有重置功能。

·初始化連通（Initially Connected）有限狀態機：如果一個FSM可以從初始狀態到達每一個狀態，則稱該FSM是初始化連通的。

·強連通（Strongly Connected）有限狀態機：如果對于FSM中的每一對狀態(S_i,S_j)，都存在一個輸入序列使得狀態S_i可遷移到狀態S_j，則稱該FSM是強連通的。

按是否使用輸入信號，有限狀態機可以劃分為：

·Mealy機：輸出信號不僅與當前狀態有關，而且還與所有的輸入信號有關，即可以把Mealy型有限狀態機的輸出看成當前狀態和所有輸入信號的函數。

·Moore機：輸出信號僅與當前狀態有關，即可以把Moore型有限狀態機的輸出看成當前狀態的函數。

按轉換狀態和輸出是否確定，有限狀態機可以劃分為：

·DFSM：對于特定的輸入和所有的狀態，轉換狀態和輸出是確定的。

·NFSM：對于特定的輸出和已經存在的狀態，轉換狀態和輸出是不確定的。

有限狀態機的表示法主要有三種：圖形法、表格法和矩陣法，其中圖形法較為常用。

有限狀態機的優點是相對簡單、可預測、易于實現和易于測試。有限狀態機的缺點是：①處理復雜問題時，有可能發生狀態空間爆炸；②在多有限狀態機系統中，系統的狀態為所有有限狀態機狀態的笛卡兒積，系統的狀態數具有狀態組合復雜性問題，且會出現死鎖；③有限狀態機可以較好地描述狀態間的遷移特性，但不能很好地描述輸入、輸出間的變換特性（即數據的變換特性）；④有限狀態機只反映了協議事件和協議狀態之間的關系，不能表達其他協議元素，如協議變量、協議行為、謂詞等。

3.擴展有限狀態機

對有限狀態機進行擴展的主要目的是增強有限狀態機的描述能力并簡化描述，使各狀態之間的變化清晰化，最終提高對局部以致整個模型的描述與分析能力，可作為工具用于后續開發者的描述和解決方案。常見的擴展有限狀態機模型有以下四種：NFSM（Non-deterministic FSM）、CFSM（Communicating FSM）、EFSM（Extended FSM）、CEFSM（Communicating EFSM）、PFSM（Probability FSM）。模型擴展的演變過程如圖3-5所示。

圖3-5　幾種常見的FSM擴展模型

其中，EFSM是軟件測試中相對較為常用的一種。一個EFSM可以表示為一個六元組<S,S₀,I,O,T,V>：

·S：非空的有限狀態的集合。

·S₀：狀態中的一種，是所有狀態的初態。

·I：非空的輸入消息集合。

·O：非空的輸出消息集合。

·T：非空的狀態遷移集合，且有t∈T，且t=<Head(t),I(t),P(t),operation/O(t),Tail(t)>。其中，Head(t)是遷移t的出發狀態；I(t)是輸入集I中包含的EFSM的輸入消息，它可以為空；P(t)是遷移t執行的前置條件，它可以為空；operation是狀態遷移過程中進行的操作，它一般由一系列的變量賦值語句或輸出語句組成；O(t)是輸出集O中包含的消息輸出，它可以為空；Tail(t)是遷移t的到達狀態。

·V：變量的集合，可表示為V=<IV,CV,OV>。其中，IV代表輸入變量集合，輸入變量可以由測試人員控制；OV代表輸出變量集合；CV代表環境變量集合，環境變量可以是局部變量或全局變量，既不是輸入變量也不是輸出變量的變量都可以歸為環境變量。CV和OV是不受測試人員控制的，它們的值由狀態遷移的操作來確定。

由EFSM的定義可見，它在FSM模型的基礎上增加了變量、操作、遷移的前置條件等。EFSM有存儲功能，它的每個狀態都有默認的重置（Reset）功能，即δ(S_i,r)=S₀。通過EFSM模型，可更加精確地描述軟件系統的行為，因此可廣泛應用于面向對象軟件系統中對象的行為以及對象之間的交互。EFSM較好地克服了上述FSM缺點中的后兩點，但還沒有解決一致性、可達性、同步等問題，并且引入了新的問題——不確定性問題。