軟體驗證工具所要檢驗的安全性質，即為檢查程式進行時，不良的狀態是否 永遠不會發生。
ArCats 進行安全性質檢驗的技術[34]，採用的是 image automata 這類自動狀 態機。image automata 是由 property automata 所衍生而來。一般檢驗的系統性質
稱為 property automata，如果子系統是正確執行，則執行順序會符合 property automata 所描述的特性。當子系統執行順序無法符合 property automata 時，image automata 就會進入我們不願意發生的狀態，例如 deadlock 或 mutual exclusion，
我們將這樣的狀態簡稱為π。
以 Figure 3-6 為例，當系統加入安全性質的檢查時，如果行程是正確執行，
若產出的合法字串應為 a,b,b,b…，符合 Figure 3-6(a)所描述的特性。若產生字串 為 a,b,b,b,b,a 時，即表示系統違反安全性質，進入不良狀態π。
Figure 3-6 (a) Property Automata (b) Image Automata
3.3.1. 安全性質的合成規則
本節將以 Figure 3-7 說明如何運用 Section 3.1 中的 Com1 和 Com2，以及安 全性質的合成規則（以 Com4 表示）這三種合成規則，進行具有檢驗安全性質功 能的局部性分析，我們將檢驗安全性質的 Image Automata，以 SP 表示
Com 1
Figure 3-7 Compose processes A and B, and SP
平行合成的初始狀態為(000)，(000)狀態中的第一個 transition 上的 label 為 a，我們將 a 這個 label 逐一做 Com1、Com2 和 Com4 三種合成規則的檢查。由 於 a 不存在於 export set 中，不符合 Com1，所以我們繼續檢查 Com2 的合成規則。
狀態(000)的第二個 transition 為-a，和 a 為一配對行為，故符合 Com2，所以 我們將此內部行為以τ 表示。由於此例中我們加入了安全性質的檢驗，故我們會
到 SP 中去檢查此步驟是否會到達不良狀態π。
此時 SP 中狀態為 0，且在此狀態上有一個 transition 的 label 為 a，和我們欲 檢查的行為 a 相同。SP 可藉由 a 由狀態 0 到達狀態 1。所以我們可以運用 Com4 的規則，使得(A || B)的平行合成結果會從狀態(000)，經由 transition 的 label τ，
到達新狀態(111)，如 Figure 3-8。由於此新狀態不會產生不良狀態π，所以我們 將此新狀態(111)加入 vector 中，以待後續繼續拓展。如果產生的新狀態包括π，
我們會顯示在(A || B)的平行合成結果中，但此狀態不會再加入 vector，因為包括 π的狀態我們就不會再繼續展開。
Figure 3-8 Composition of (A || B) by Com2 and Com4
由於狀態(000)尚未有 transition 沒檢查完畢，所以我們繼續檢查第二個 transition 上的 label -a。-a 存在於 export set 中，符合 Com1。於是我們繼續進行 安全性質合成規則 Com4 的檢查，此時 SP 的狀態為 0，且狀態 0 上有一個 transition
的 label 為 a，可以使狀態 0 到達狀態 1，且狀態不包含π。所以經由 Com4 的合 成規則，(A || B)的平行合成結果會從狀態(000)，經由 transition 的 label -a，到達 一新狀態(011)，如 Figure 3-9 所示。
Figure 3-9 Composition of (A || B) by Com1 and Com4
利用上述三項合成規則反覆檢查每一個狀態的 transition 後，(A || B)的最後平 行合成結果如 Figure 3-10 所示，其中有一狀態(21π)，表示該子系統的執行順序 會進入不良狀態，違反安全性質。
Figure 3-10 Composition of (A || B) with checking Safety Property