鄭永斌Yung-Ping Cheng程郁如2019-08-292005-8-232019-08-292005http://etds.lib.ntnu.edu.tw/cgi-bin/gs32/gsweb.cgi?o=dstdcdr&s=id=%22G0069108009%22.&%22.id.&http://rportal.lib.ntnu.edu.tw:80/handle/20.500.12235/92665在局部分析(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 這幾方面的實作加以闡述。Compositional AnalysisContext ConstraintState ExplosionHierarchical TracingExplicit Compositional State-Space Enumeration with Context Constraint& Counter Examples by Hierarchical Tracing