(3.235.191.87) 您好!臺灣時間:2021/05/13 05:00
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:蔡明憲
研究生(外文):Ming-Heisn Tsai
論文名稱:假設保證式模組化驗證方法之自動化
論文名稱(外文):Automation of Modular Verification Using the Assumption-Guarantee Approach
指導教授:蔡益坤
指導教授(外文):Yih-Kuen Tsai
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:資訊管理學研究所
學門:電算機學門
學類:電算機一般學類
論文種類:學術論文
論文出版年:2004
畢業學年度:92
語文別:英文
論文頁數:59
中文關鍵詞:時態邏輯模組化驗證複雜度假設保證驗證
外文關鍵詞:verificationcompositionassumption-guaranteemodel checkingtemporal logic
相關次數:
  • 被引用被引用:0
  • 點閱點閱:92
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
模組化軟體設計的正確性引發模組化驗證的需求。由於某個特定軟體設計的其中一個模組不一定會知道其他模組的實際運作內容,所以對於這樣的驗證工作,假設保證式之推論可作為一個良好的架構。在本篇論文裡,我們深究如何透過模型檢驗的方法,將使用QPTL(定量命題時態邏輯)來描述假設保證式系統規格之模組化驗證予以自動化。雖然QPTL對於系統規格的描述能力相當強大,但檢驗一個QPTL式子的正確性卻具有相當高的複雜度,這主要導因於將系統變數予以定量。此外,近代在時態邏輯方面的模型檢驗工具並不支援這種定量方式。我們於本篇論文中展示如何將定量消除,使得模型檢驗工具可以被用來完成模組化驗證工作的自動化。我們也建立兩個小型例子作為本方法的說明範例。
Correctness of a component-based software design induces the need
of modular verification. As one component of a design may not know
the implementation details of others, assumption-guarantee
reasoning serves as a good framework for such verification tasks.
In this thesis, we investigate the automation of modular
verification, achieved by converting such problems to model
checking problems, using assumption-guarantee specifications
written in quantified propositional temporal logic (QPTL). Though
QPTL is very expressive, the complexity of checking the validity
of a QPTL formula is extremely high, which is mainly caused by the
existence of quantifications over program variables. Besides,
modern model checkers for temporal logic do not support such
quantifications. We show how these quantifications can be
eliminated so that model checkers can be used to automate the
modular verification tasks. Two small examples are constructed for
illustration of the approach.
Contents
1 Introduction 1
2 Related Work 3
2.1 Temporal Logic. . . . . . . . . . . . . . . . 3
2.2 Symbolic Model Checking . .. . . . . . . . . 4
2.3 Modular Verication . . .. . . . . . . . . . . 5
3 Preliminary 7
3.1 Finite-State Automata . . . . . . . . . . . . 7
3.2 Propositional Temporal Logic . . . . . . . .. 7
3.2.1 Linear Temporal Logic . . . . . . . . . . . 8
3.2.2 Quantified Propositional Temporal Logic . . 10
3.3 Assumption-Guarantee Specications . . . . . . 11
3.4 An Introduction to NuSMV . . . . . . . . . . .13
3.4.1 MODULE Declarations . . . . . . . . . . . . 14
3.4.2 VAR Declarations . . . . . . . . . . . . . 14
3.4.3 DEFINE Declarations . . . . . . . . . . . . 15
3.4.4 ASSIGN Declarations . . . . . . . . . . . . 15
3.4.5 LTLSPEC Declarations . . . . . . . . . . . 16
3.4.6 Simple Expressions . . . . . . . . . . . . 16
3.4.7 Next Expressions . . . . . . . . . . . . . 17
3.4.8 Identiers . . . . . . . . . . . . . . . . . 18
4 Modular Verification with A-G Specifications 19
4.1 The KEEP-AHEAD Example . . . . . . . . . . . . . . . . . . . . . 19
4.1.1 Description . . . . . . . . . . . . . . . . 19
4.1.2 A-G Specifications . .. . . . . . . . . . . . 20
4.2 The TOKEN-RING Example . . . . . . . . . . . 21
4.2.1 Description . . . . . . . . . . . . . . . . 21
4.2.2 A-G Specifications . . . . . . . . . . . . . 25
5 Automation of Modular Verification Using NuSMV 31
5.1 The KEEP-AHEAD Example . . . . . . . .. . . . 31
5.2 The TOKEN-RING Example . . . . . . . . . . . .33
6 Conclusion 38
6.1 Contributions 38
6.2 Future Work 39
Bibliography
[1] M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Program-
ming Languages and Systems, 15(1):73-132, January 1993.
[2] M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Program-
ming Languages and Systems, 17(3):507-534, May 1995.
[3] B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters,
24(4):181-185, October 1985.
[4] N. Amla, R. P. Kurshan, K. L. McMillan, and R. Medel. Experimental analysis of
different techniques for bounded model checking. In Proceedings of TACAS, LNCS
2619, pages 34-48. Springer-Verlag, 2003.
[5] M. Benedetti and A. Cimatti. Bounded model checking for past ltl. In Proceedings of
TACAS, LNCS 2619, pages 18-33. Springer-Verlag, 2003.
[6] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs.
In Proceedings of TACAS, LNCS 1579, pages 193-207. Springer-Verlag, 1999.
[7] R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986.
[8] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic Model
Checking: 1020 States and Beyond. In Proceedings of the Fifth Annual IEEE Symposium
on Logic in Computer Science, pages 1-33, Washington, D.C., 1990. IEEE Computer
Society Press.
[9] A. Cimatti, E. M. Clarke, F. Giunchiglia, and M. Roveri. NuSMV: A new symbolic model
checker. International Journal on Software Tools for Technology Transfer, 2(4):410-425,
2000.
[10] E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using
branching time temporal logic. In Proceedings of Workshop on Logics of Programs,
LNCS 131, pages 52-71, 1981.
[11] E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, 1999.
[12] E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 353-362,
1989.
[13] D. Gabbay, A. Pnueli, S. Shelah, , and J. Stavi. On the temporal analysis of fairness. In Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of
Programming Languages, pages 163-173. ACM Press, 1980.
[14] C.B. Jones. Specification and design parallel programs. In Information Processing 83,
pages 321-332, 1983.
[15] B. Jonsson and Y.-K. Tsay. Assumption/guarantee specifications in linear-time temporal
logic. Theoretical Computer Science, 167:47-72, October 1996. An extended abstract
appeared earlier in TAPSOFT ''95, LNCS 915.
[16] J. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Dept. of Computer
Sciences, University of Texas, Austin, Tx 78712., May 1987.
[17] Y. Kesten and A. Pnueli. Complete proof system for QPTL. Journal of Logic and
Computation, pages 97-109, June 2001.
[18] Y. Kesten, A. Pnueli, and L. Raviv. Obdd''s ltl mc model checking of linear tl, using
obdd''s. Technical report, Weizmann Institute of Science, 1995.
[19] L. Lamport. Specifying concurrent program modules. ACM Transactions on Program-
ming Languages and Systems, 5(2):190-222, 1983.
[20] L. Lamport. The temporal logic of actions. ACM Transactions on Programming Lan-
guages and Systems, 16(3):872-923, May 1994.
[21] F. Laroussinie, N. Markey, and P. Schnoebelen. Temporal logic with forgettable past,
2002.
[22] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems:
Specification. Springer-Verlag, 1992.
[23] Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-
Verlag, 1995.
[24] J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on
Software Engineering, 7(4):417-426, July 1981.
[25] M. W. Moskewicz, C. F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff:
Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation
Conference (DAC''01), 2001.
[26] A. Pnueli. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium
on Foundations of Computer Science, pages 46-67, 1977.
[27] C. Szyperski. Component Software: Beyond Object-Oriented Programming. Addison-
Wesley, 1998.
[28] J.-W. Teng and Y.-K. Tsay. Composing temporal-logic speci‾cations with machine
assistance. In K. Araki, S. Gnesi, and D. Mandrioli, editors, Proceedings of the 12th
International Formal Methods Europe Symposium (FME 2003), LNCS 2805, pages 719-738. Springer, September 2003.
[29] Y.-K. Tsay. Compositional verification in linear-time temporal logic. In J. Tiuryn, editor,
Proceedings of the Third International Conference on Foundations of Software Science
and Computation Structures, LNCS 1784, pages 344-358. Springer, March 2000.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
系統版面圖檔 系統版面圖檔