實作應用於局部分析中的即時化減技術

Abstract

在軟體驗證領域中，模型檢測（Model Checking）技術是最被認可的方法之一，但最常遇到的困難，就是在建構系統模型時，常因記憶體資源不足而發生組態爆炸的問題（State Explosion Problem）。故為了提升模型檢測的可行性，有人提出局部分析（Compositional Analysis），這類技術利用原本系統的架構將一個大系統分割成許多子系統，以階層的方式來做驗證，並有效減少子系統中不必要的內部行為（internal behaviors），以避免一次整體分析可能造成的組態爆炸問題。

然而，局部分析還是有發生組態爆炸的可能性，如系統的階層架構不良，或是切割的子系統仍舊太大，都極可能讓局部分析失效。故在這篇論文中，我們選用Branching Bisimulation Minimization的化減技術，以得到一個組態空間較小但表現行為等價的系統模型。且Branching Bisimulation具有許多優於其他等價關係的特性，化減後仍可保留系統模型的必然性（liveness），其演算法也具有較佳的效率。然而，傳統的化減技術都是預設子系統模型已存在的情況下來執行，但大部分實際情況，在建構子系統時即已發生組態爆炸的問題。故我們提出即時化減的技術—On-the-fly Branching Bisimulation Minimization，在建構模型的過程中即先行化減的動作，讓內部行為所佔的記憶體空間，在狀態展開的過程中即可被釋放出來，以避免組態爆炸，而有效提高局部分析的可行性。Model checking is a promising approach to analyze concurrent programs. However, enumerating the whole system model at once often leads to the problem of state explosion. In order to make it more practical, compositional analysis is presented. It verifies a system model in a hierarchical manner, and reduces unconcerned internal behaviors after each composition of subsystem.

In our thesis we choose the Branching Bisimulation Minimization [26][27] to obtain a smaller but equivalent model with regard to the original composed one. Branching Bisimulation has several nice properties better than other equivalences. It preserves liveness properties and allows more efficient algorithm to be built. Nonetheless, Branching Bisimulation Minimization is typically performed after the whole state space is enumerated completely. In the worst case, explored state space can already trigger state explosion even it can be minimized considerably. So, we propose an on-the-fly Branching Bisimulation Minimization which is integrated with our parallel composition engine. It minimizes the state space while composing to certain extent, and releases unnecessary memory space for further state enumerations. This approach alleviates the state explosion problem, therefore, increase the scalability of compositional analysis because internal behaviors in a composed subsystem can be reduced intermediately.