2 彈性和擴充性

重構後的系統所帶來的好處不僅只有整理原有的程式碼，將其變得更清晰易 懂。更重要的在於，重構後對於系統的彈性和擴充性提高，對於後續系統的開發 與維護將會產生更明顯的助益。

5.2.1. 合成規則的組合與加入即時化減技術

若我們要在原有的系統進行 CCS 安全性質的檢驗時，加入一併執行即時化 減的功能。在假設 CCS 檢驗安全性質時進行即時化減技術，不會影響原有 CCS 安全性質與即時化減理論上的運用的前提下。重構前的系統架構在新增此項功能 時，等於要新增一個相對應的函式，以供主程式呼叫。並且以 copy-paste 的方式，

在既有的 SafetyProperty()函式中，進行即時化減功能的修改。而這些功能的新增 與修改，必須藉由 EnumerationWithStateBB()、EnumerationWithMemoryBB()和

EnumerationWithLevelBB()，這三個函式中有關即時化減技術的程式碼。才能實 作出三個新的函式 SafetyPropertyWithStateBB()、SafetyPropertyWithMemoryBB() 和 SafetyPropertyWithLevelBB()的新增，以供主程式呼叫。

由於原系統新增功能時必須以 copy-paste 的方式撰寫，所以我們以原有的函 式 SafetyProperty()、EnumerationWithStateBB()、EnumerationWithMemoryBB()和

EnumerationWithLevelBB()這四個函式中既有的程式碼做估算，重構前的系統若 欲新增檢驗安全性質時，同時進行即時化減的功能，必需再額外撰寫約 500 行的 程式碼。

而在重構後的系統中，由於合成規則和即時化減技術選項是以組合的方式，

分別由 Rule Engine 和 Minimization Engine 各別運作。如果要新增檢驗安全性質 時，同時進行即時化減的功能，我們只要同時給定安全性質和即時化減技術的參 數，不用再新增任何程式碼，系統即可立即進行分析。所以新增此功能所需的額 外的程式碼是 0 行。以上的比較的結果我們以 Table 6 說明。

程式碼 新增功能 新增程式碼行數

重構前

系統 CCS Safety Property with StateBB CCS Safety Property with LevelBB CCS Safety Property with MemoryBB

約 500 行 重構後

系統 約 0 行

Table 6 The compare of adding minimization option in composition rule

在系統進行分析時，若我們希望加入同時進行本文限制和安全性質的檢驗，

也就是兩個合成規則之間的組合。同樣地，我們假設兩個合成規則同時運作時，

和該合成規則單獨運作時，所持有的理論邏輯是相同的。那麼在重構前的系統 中，我們必須將原有 ContextConstraint()和 SafetyProperty()兩支函式的程式碼以 copy-paste 的方式修改，綜合成一支具有複合合成功能的函式，以供主程式呼叫。

我們也依既有的程式碼進行估算，可以得知如果要在重構前的系統中新增

ContextConstarintWithSafetyPropery()的函式，必需再新增加約 500 行的程式碼。

對於重構後的系統而言，如果要新增同時進行本文限制和安全性質的檢驗，

在理論不會因而改變的情況下，我們也無需新增任何程式碼，直接讓使用者設定 參數，以原有的程式碼運作即可。事實上，重構後的系統只有在組合合成規則之 後，會造成理論運作時細節的改變，才需要對程式碼做適當的修改或處理。而重 構前的系統中，無論合成規則之間的組合，在理論上的操作會不會有變化，都必 須要撰寫新的程式碼因應，這是由於原有的架構無法使得程式碼可以重覆利用，

所造成後續系統開發上的負擔，以上的比較我們以 Table 7 說明。

程式碼 新增功能 新增程式碼行數

重構前

系統 CCS ContextConstraintWithSafetyProperty

約 500 行 重構後

系統 約 0 行

Table 7 The compare of combination of composition rules

5.2.2. 新增 LTS 型態

除了在合成規則中新增即時化減的功能，或是合成規則之間的組合之外，在 之前的章節中我們也有提到，ArCats 的局部性分析工具希望在使用者建立系統模 型時，可以提供更多彈性，所以未來希望加入 CSP 的合成規則，以進一步分析 CSP 的 LTS 模型。

我們除了在系統中加入 CSP 的基本合成規則，使得 CSP 可以具有平行合成，

也就是 enumeration 的功能之外。我們並希望 CSP 可以具有如同 CCS 相同的分 析功能：本文限制、安全性質檢驗、即時化減技術，以及前述這些合成規則之間 可能的組合。

我們假設 CCS 和 CSP 在本文限制、安全性質和即時化減技術等理論上的運 作基本上都是相同的。在重構前的系統中，原有的 CCS 本文限制、安全性質和 即時化減技術的程式碼，完全無法直接讓 CSP 此新的 LTS 型態重覆使用，必需 要將全部的程式碼重新撰寫。而以既有 CCS 程式碼所能達到的功能來估算，加 入 CSP 後所需要重新撰寫的程式碼約有 2000 行以上。

而在重構後的系統加入 CSP 的合成規則，由於假設本文限制和安全性質的 理論操作都相同，所以程式碼可以不用修改。僅需新增 CSP 中有關模型溝通方 式的合成規則，也就是在 Section 3.1 中所介紹的 Com2。因為 CSP 在並行系統的 溝通上是 multi-way rendezvous，CCS 是以 two-way rendezvous 的方式，所以 CSP 和 CCS 在基本的合成規則上僅在 Com2 的運作上有所區別。所以在重構後的系 統中，我們只需增加 CSP 有關 Com2 的規則的程式碼即可，其餘的程式碼皆無 需更動，新增的額外程式碼約在 100 行以內即可完成。我們以 Table 8 說明重構 前後的系統架構，加入 CSP 後的比較。

程式碼 新增功能 新增程式碼行數

重構前 系統

CSP Enumeration

CSP Enumeration with StateBB CSP Enumeration with MemoryBB CSP Enumeration with LevelBB CSP Context Constraint

CSP Context Constraint with StateBB CSP Context Constraint with MemoryBB CSP Context Constraint with LevelBB CSP Safety Property

CSP Safety Property with StateBB CSP Safety Property with MemoryBB CSP Safety Property with LevelBB

約 2000 行

重構後

系統 約 100 行

Table 8 The compare of adding new LTS type (CSP)