模擬結合局部性分析

Simulation with Compositional Analysis

李俊佑(Chun Yu Li)

指導教授 ： 鄭永斌

國立臺灣師範大學/教育學院/資訊教育學系/碩士(2006年)

摘要

近年來，局部性分析在自動化軟體檢驗領域中佔有一席之地，是相當有前景的研究方向。局部性分析能夠成功的關鍵在於被檢驗的系統有良好的模組架構。利用合併及最小化的技術，我們可以取得子系統的介面行程。介面行程可以忽略內部行為而代表子系統，如此重覆進行局部性分析可以藉此減緩組態爆炸。
模擬是一種樂觀性的品質保證，雖然不能證明錯誤不存在，但是它的實用性在產業界和應用領域已得到很好的例證。模擬的好處之一在於其避免記錄大量的狀態而造成實體記憶體不夠的問題。只要盡可能花時間檢驗系統模型，對系統本身的正確性就更有信心。
在本篇論文中，我們將模擬和局部性分析結合在一起。利用局部性分析所取得的介面行程，只要模擬的路徑行經它，就可以視為已經拜訪過該介面行程所代表的子系統。這樣做的好處可以大大縮減模擬拜訪的深度。我們的simulator建立在既有的ArCats架構之上，運用物件導向的多型技巧，讓模擬運行在CFG（Control Flow Graph）與CCS（Calculus of Communicating System）兩種CFSM中。本篇論文會以實際的例子說明模擬結合局部性分析的好處，同時在實驗中評估其價值。

關鍵字

模擬 ； 局部性分析 ； 模擬結合局部性分析 ； 模型驗證

並列摘要

In recent years, compositional analysis in the automatic verification techniques is known as a promising approach. The states in subsystem can be minimized and hidden to alleviate state explosion while building the interface process that represents the whole subsystem. However, the key of success relies on a good modularity in system architecture. Some systems are still not amenable to compositional analysis. Simulation is an optimistic quality assurance like testing. Simulation can avoid exhausting memory while exploring state space. In the area of hardware validation, it is practical but cannot provide assurance in absence of errors. Given enough time, critical errors may still be manifested by simulation technique.
In the paper, we combine simulation and compositional analysis together. Processes in a subsystem are composed into an interface process. Simulation that walks into the interface process is equal to walk a lot of hidden states in the subsystem. The simulator of ArCats runs in the two different graph, CFG (Control Flow Graph) and CCS (Calculus of Communicating System), with polymorphism technique in OOP. The advantages of simulation with compositional analysis are shown by examples and evaluation.

並列關鍵字

Simulation ； Compositional analysis ； Simulation with Compositional Analysis ； Model checking ； ArCats

參考文獻

[1] Holzmann, G. J. “The model checker SPIN.” IEEE Transaction on Software Engineering, Volume 23, Issue 5 : 279-295, May 1997.

[2] Holzmann, G. J. “The SPIN Model Checker: Primer and Reference Manual” Pearson Educational, 2003.

[3] Godefroid, Patrice. “Model Checking for Programming Languages using VeriSoft.” In 24th ACM Symposium onPrinciples of Programming Languages, pp. 174-186, Paris. 1997.

[4] Godefroid, Patrice. “Software Model Checking: The VeriSoft Approach.” Formal Methods in System Design 26(2): 77-101, 2005.

[5] Jurgen Dingel. “Compositional analysis of C/C++ programs with VeriSoft.” Acta informatica 43:45-71, 2006.