有窮測試

有窮狀態機用一個有向圖表示，結點表示狀態，有向邊表示狀態之間的遷移。該方法使用狀態和事件來表示面向對象編程中類的行為。一個類的狀態包含初始狀態和終止狀態。

範圍和前景

有窮測試適用於具有封裝等特徵的面向對象軟體，並可用於高層黑盒測試。在簡單類建模和測試中，任何時候至多只能存在一個對象。對於任何遷移，如果其事件是類中一個引發錯誤條件的成員函式，那么遷移的目標狀態就是錯誤狀態。如果每個錯誤條件被認為是不同的錯誤狀態，那么模型可以得到進一步推廣。

測試用例生成

一個遷移由事件、守衛條件和動作這三部分組成。一個事件表示對類成員函式的調用。守衛條件是遷移執行必須要滿足的條件，它可以是任何類數據屬性或函式調用輸入參數構成的謂詞條件。當守衛條件為真，動作就被執行。一個動作是遷移發生時將要執行的一組操作，可以引用或操作任何類數據屬性或函式調用產生的輸出參數。不論何時，在收到一個表示訊息或函式調用的事件時，對象的下一個狀態便依賴於當前狀態激發事件的內容或動作。由一個事件引起的狀態變化就稱為遷移。

假定一個類C在任何時候至多存在一個對象實例，下面給出用代數元組表示的簡單類狀態模型：M=(V,F,S,T)

式中：

V－－C的數據屬性組成的有窮集合；

F－－C的成員函式組成的有窮集合；

S－－C的狀態組成的有窮集合，即S={s:s=(predV)}，其中，predV是一個基於V中數據屬性的謂詞；

T－－遷移組成的有窮集合，即T={t:t=(source,target,event,guard,action)}，其中，源狀態source∈S，目標狀態target∈S，事件event∈F，守衛條件guard是V中屬性或F中函式參數形成的謂詞，動作action是對V中屬性或F中函式參數的一個計算。

一個簡單類狀態模型可以表示為一個有向圖，其中，S是結點集合，T中元素是從源節點到目標節點的帶標記有向邊。