簡易檢索 / 詳目顯示
| 研究生： |
程郁如 |
|---|---|
| 論文名稱： |
Explicit Compositional State-Space Enumeration with Context Constraint & Counter Examples by Hierarchical Tracing |
| 指導教授： |
鄭永斌
Cheng, Yung-Pin |
| 學位類別： |
碩士 Master |
| 系所名稱： |
資訊教育研究所 Graduate Institute of Information and Computer Education |
| 論文出版年： | 2005 |
| 畢業學年度： | 93 |
| 語文別： | 英文 |
| 論文頁數： | 74 |
| 中文關鍵詞： | Compositional Analysis 、Context Constraint 、State Explosion 、Hierarchical Tracing |
| 論文種類： | 學術論文 |
| 相關次數： | 點閱：220 下載：0 |
| 分享至: |
| 查詢本校圖書館目錄 查詢臺灣博碩士論文知識加值系統 勘誤回報 |
在局部分析(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 這幾方面的實作加以闡述。
Reference
[1] Alur, Rajeev and Brayton, Robert K. and Thomas A. Henzinger and Shaz
Qadeer and Sriram K. Rajamani. Partial-Order Reduction in Symbolic State
Space Exploration. CAV 1997, pp. 340-351.
[2] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
[3] Clarke, E. M., Emerson, E.A., and Sistla, A. P. Automatic Verification of
Finite-State Concurrent Systems Using Temporal Logic. TOPLAS, vol.8, no.2,
APR, page224-263, 1986.
[4] Clarke, E. M., Grumberg, O. and Peled, Doron A. Model Checking. MIT Press,
2000.
[5] Corbett, James C. Evaluating deadlock detection methods for concurrent
software. IEEE Transactions on Software Engineering, 2(3):161-180, March
1996.
[6] Duri, S., Buy, U., Devarapalli R., and Shatz, S.~M. Using State Space
Reduction Methods for Deadlock Analysis in Ada tasking. ISSTA, June 28-30,
1993, 51-60.
[7] Glabbeek, R. v. and P. Weijland. Branchinging time and abstraction in
bisimulation semantics (extended abstract). In information Processing 89, G.
Ritter, ed., North-Holland, pp. 613-618, 1989.
[8] Godefroid, P. and Wolper, P. A Partial Approach to Model Checking. LICS
1991, pp. 406-415.
[9] Graf, S. and Steffen, B. Compositional Minimization of Finite State Systems. pp.
186-196, CAV 1990.
[10] H. Y. Wang. On-the-fly Bisimulation Minimization in Compositional Analysis.
Master Thesis. Dept. of Info. And Comp. Edu. NTNU, 2005.
[11] Holzmann, G. J. The model checker SPIN. IEEE Trans. Softw. Eng.,
23(5):279-295, May 1997.
[12] J. C. Corbett, M. B. Dwyer, J. Hatcliff, S. Laubach, C. S. Pasareanu, Robby,
and H. Zheng. Bandera: extracting finite-state models from java source code.
In International Conference on Software Engineering, pages 439-448, 2000.
[13] K. Havelund and T. Pressburger. Model checking JAVA programs using JAVA
pathfinder. International Journal on Software Tools for Technology Transfer,
2(4):336-381, 2000.
[14] Krishan K. Sabnani, Aleta M. Lapone, and M. Umit Uyar. An algorithmic
procedure for checking safety properties of protocols. IEEE Transactions on
Communications, 37(9):940-948, September 1989.
[15] Madelaine, E. and Simone, R. de. The FC2 Reference Manual.
ftp://a.fr:pub/verifi as file fc2refman.ps, INRIA.
[16] Marcelo Fiore, Gian Luca Cattani, Glynn Winskel. Weak Bisimulation and
Open Maps. Proceedings of the 14th Symposium on Logic in Computer
Science, p.67, July 02-05, 1999.
[17] McMillan, K. L. Symbolic Model Checking. Kluwer Academic Publishers.
Boston 1993.
[18] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
[19] Robin, Milner. A Calculus of Communicating Systems. volume 92 of Lecture
Notes in Computer Science. Springer-Verlag, New York, 1980.
[20] S. C. Cheung and J. Kramer. Context constraint for compositional reachability
analysis. ACM Transactionson on Software Engineering and Methodology,
5(4):334-377, October 1996.
[21] S. C. Cheung and J. Kramer. Checking safety properties using compositional
reachability analysis. ACM Transactions on Software Engineering and
Methodology, 8:49-78, January 1999.
[22] S. C. Cheung and D. Giannakopoulou and J. Kramer. Verification of liveness
properties using compositional reachability analysis. In 5th ACM SIGSOFT
Symposium on Foundations of Software Engineering, pages 227-243, Zurich,
Switzerland, September 1997.
[23] Sistla, A. P. and Gyuris, K. and Emerson, E. A. {SMC} : a symmetry-based
model checker for verification of safety and liveness properties. ACM
Transactions on Software Engineering and Methodology, vol. 9, no. 2, pp.
133-166, 2000.
[24] Vardi, Moshe Y. and Wolper, Pierre. An automata-theoretic approach to
automatic program verification. Proc. First IEEE Symp. On Logic in Computer
Science, 1986, pp. 323-331.
[25] Yeh, W.-J. and Young, M. Compositional Reachability Analysis Using Process
Algebra. TAV4, pp. 49-59, 1991.
[26] Yeh, W.-J. and Young, M. Hierarchical Tracing of Concurrent Programs.
SERC-TR-137-P, March, 1993.
[27] Yeh, W.-J. and Young, M. Re-designing Tasking Structure of Ada programs for
Analysis : a Case Study. Software Testing, Verification, and Reachability, Vol. 4,
pp. 223-253, 1994.
[28] Y.-P. Cheng. Grafting a Promela Front-End with Abstract Data Types to
Mitigate the Sensitivity of Compositional Analysis to Implementation Choices.
NTNU, Taipei, Taiwan, 2005.
[29] Y.-P. Cheng. Refactoring Design Models for Inductive Verification. Proceedings
of the ACM SIGSOFT 2002 International Symposium on Software Testing and
Analysis. Rome, Italy, July 22-24, 2002.
[30] Y.-P. Cheng and M. Young. Semi-Automated Refactoring of Design Models for
Compositional Analysis. Working Conference on Complex and Dynamic
Systems Architecture, pp. 137-139, Brisbane, Australia, December, 2001.
[31] Y.-P. Cheng, M. Young, C.-L. Huang, and C.-Y. Pan. Towards scalable
compositional analysis by refactoring design models. In proceedings of the ACM SIGSOFT 2003 Symposium on the Foundations of software Engineering,
pp. 247-256, 2003.