Explicit Compositional State-Space Enumeration with Context Constraint& Counter Examples by Hierarchical Tracing
No Thumbnail Available
Date
2005
Authors
Journal Title
Journal ISSN
Volume Title
Publisher
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 這幾方面的實作加以闡述。
Description
Keywords
Compositional Analysis, Context Constraint, State Explosion, Hierarchical Tracing