蔡益坤臺灣大學：資訊管理學研究所蔡明憲Tsai, Ming-HeisnMing-HeisnTsai2007-11-262018-06-292007-11-262018-06-292004http://ntur.lib.ntu.edu.tw//handle/246246/54306模組化軟體設計的正確性引發模組化驗證的需求。由於某個特定軟體設計的其中一個模組不一定會知道其他模組的實際運作內容，所以對於這樣的驗證工作，假設保證式之推論可作為一個良好的架構。在本篇論文裡，我們深究如何透過模型檢驗的方法，將使用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 39396402 bytesapplication/pdfen-US時態邏輯模組化驗證複雜度假設保證驗證verificationcompositionassumption-guaranteemodel checkingtemporal logicotherhttp://ntur.lib.ntu.edu.tw/bitstream/246246/54306/1/ntu-93-R91725014-1.pdf