Explicit Compositional State-Space Enumeration with Context Constraint& Counter Examples by Hierarchical Tracing

Abstract

在局部分析(Compositional Analysis)技術中，在合成展開一個代表子系統行 為的狀態空間(State Space)時，這個合成展開的過程中必須要加入本文限制 (Context Constraint)與簡化子系統(Reduction or Minimization)的技術來降低組態 爆炸(State Explosion)的問題。然而，目前為止，已知的驗證工具對局部分析的 支援還是很稀少。這些少數支援局部分析的工具通常操作過程繁複，一般使用 者很難上手。 在本篇論文中，我們根據既有的理論與技術，開發實做出一個較為容易使 用的工具套件。其中，我們實做了本文限制(Context Constraint)的技術來消除子 系統內多餘的狀態。除此之外，為了降低子系統展開的狀態空間的規模，我們 另外提出了一個以Branching Bisimulation 關係為基礎的on-the-fly Branching Bisimulation技術，用來在展開的過程中去簡化子系統的狀態空間。另外，我們 發展出來的工具，還根據了階層式追蹤(Hierarchical Tracing)的演算法實做出階 層追蹤的功能，此功能能夠提供關於分析結果的完整資訊給使用者。本篇論文 將對本文限制(Context Constraint)、階層式追蹤(Hierarchical Tracing)與支援 on-the-fly Branching Bisimulation 這幾方面的實作加以闡述。