49
第五章 結論與未來工作
5.1. 結論
使用模擬結合局部性分析的好處正如我們所預期的，可以減少模擬所需拜訪 的狀態空間。對於原先有模型重構（model architecture refactoring）能力的 ArCats 來說，模擬的功能不僅使 ArCats 更加完整，也使模擬可應用的範圍更多更廣。
猶如在 4.3 節的實驗數據，我們更有信心模擬結合局部性分析的成效是視局部性 分析的程度而增加。不管單就在狀態空間中所佔的量，或是在佔整個系統的比 例，理論上在模組性良好的前提下，局部性分析的子系統愈多，模擬需要拜訪的 路徑愈少。
模擬既然不能保證錯誤的不存在，就表示它不能取代驗證原有可以達到的成 效。雖然我們在本篇論文中得到正面的成果，但仍要小心注意並不是所有的系統 都適合使用模擬。在什麼時候、什麼系統中要使用模擬或使用驗證端看使用者的 策略。一個適當的檢驗策略可能需要許多實務經驗的累積，而且也才能夠讓系統 符合實用性的目的。實用性不僅代表是不是普及和受歡迎，也代表所付上的代價 和其價值是否相符。舉例來說，醫療系統和自動販賣機系統可能就各自適合不同 的檢驗策略。
在本篇論文裡，我們嘗試將模擬與局部性分析結合在一起，讓使用者在檢驗 系統的策略上多一種可能的選擇。對部分的系統來說，某些部分可能是極為重要
50
的系統核心，不容許任何錯誤產生；某些部分也許就不需要那麼嚴謹。模擬結合 局部性分析用在模組性架構良好的系統上（或是 ArCats 可重構的系統上）。良好 的模組性能夠盡可能取得最小的子系統介面行程，在模擬的時才能充分減低需要 運算的深度。相反地，若是介面行程與原有的子系統狀態數目差異不大，模擬的 成效就大幅減低。因此在檢驗之前應要審慎評估該系統是否適用模擬結合局部性 分析。
5.2. 未來工作
目前，ArCats 模擬的檢驗能力僅限於 deadlock。我們預期應該可以將檢驗 livelock、assertion 功能加入。直覺上，偵測 Livelock 可能的限制是需要使用者訂 定探測的深度（depth），在一定的範圍內尋找行程運行打轉的證據。在此前提之 下，如果欲檢測的系統過於龐大，探測的深度就會因為需要記錄一定程度的狀態 空間，而受限於實體記憶體的大小。Assertion 的處理初步可以分為兩類，一類是 在建構模型的初期，就將欲加入的 assertion 放入模型當中。一般來說，這類方法 應該要注意 assertion 置入點不能影響原始系統並行化的行為。另一類是利用對 symbol table 內容的監控，找出變數或 channels 異常的變化。加入 livelock 及
assertion 的功能，ArCats 的模擬檢驗能力會更完備。
如何減少模擬拜訪的路徑亦是可以研究的課題。與其他驗證工具不同的，
ArCats 模擬功能是遊走在 CFG 和 CCS 之間。在 VeriSoft 中所採用的方式是 partial
order 來引導 simulator 拜訪這些狀態，但是 partial order 必須符合一個假設，也就
51
是所要檢驗的系統特質與這些排列的順序無關。ArCats 的模擬也許可以採用 partial order 的做法，但是要考量 CFG 和 CCS 兩種不同型態的系統模型是否能適 用在同一種方法；同時，亦要重新思考兩者資料結構是否可以利用物件導向的多 型機制。
另外，利用子系統的介面與界限，我們可以將子系統的行程轉換成 CCS。
但在轉換的過程中會牽涉到許多問題，例如符號擴展（symbolic expansion）。如 果要將重要的變數內容加入到模型中，常常需要將變數所有可能值都一一展開。
在設計時如果考量不周延，使用範圍最大的變數，轉換變數的可能範圍就會過 大，也會產生過大的 CCS。此時，就算子系統的行程個數已被大量減少，最後 產生的介面行程仍可能會異常大。將來可能可以發展一套方法，不進行 CFG 到 CCS 的轉換而直接進行 CFG 的合成。合成的過程中若可以直接考慮變數所有的 可能值，則可以排除符號擴展的困擾，所產生的 CFG 亦可以供 simulator 使用。
CFG 的合成很可能不是容易的問題，對被合成行程所造成的影響和效應也需要 嚴格考慮；但未來的研究若有成果，也會將模擬檢驗可應用的範圍提高一個層次。
