請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/83194完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 蔡益坤 | zh_TW |
| dc.contributor.advisor | Yih-Kuen TSAY | en |
| dc.contributor.author | 蘇俊杰 | zh_TW |
| dc.contributor.author | Chun-Jie Su | en |
| dc.date.accessioned | 2023-01-10T17:15:23Z | - |
| dc.date.available | 2023-11-09 | - |
| dc.date.copyright | 2023-01-07 | - |
| dc.date.issued | 2022 | - |
| dc.date.submitted | 2002-01-01 | - |
| dc.identifier.citation | Sheldon B. Akers. Binary decision diagrams. IEEE Transactions on computers, 27(06):509–516, 1978. Tomáš Babiak, Mojmír Křetínskỳ, Vojtěch Řehák, and Jan Strejček. LTL to Büchi automata translation: Fast and more deterministic. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 95–109. Springer, 2012. Jiří Barnat, Luboš Brim, Ivana Černá, Pavel Moravec, Petr Ročkai, and Pavel Šimeček. Divine–a tool for distributed verification. In International Conference on Computer Aided Verification, pages 278–281. Springer, 2006. Jerry R Burch, Edmund M Clarke, Kenneth L McMillan, David L Dill, and Lain-Jinn Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992. Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: a new symbolic model checker. International Journal on Software Tools for Technology Transfer, 2(4):410–425, 2000. Edmund Clarke, K McMillan, Sérgio Campos, and Vasiliki Hartonas-Garmhausen. Symbolic model checking. In International Conference on Computer Aided Verification, pages 419–422. Springer, 1996. Edmund M Clarke and E Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logic of Programs, pages 52–71. Springer, 1981. Costas Courcoubetis, Moshe Vardi, Pierre Wolper, and Mihalis Yannakakis. Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1(2):275–288, 1992. Daniel Dietsch. Automated verification of system requirements and software specifications. PhD thesis, Albert-Ludwigs-Universität Freiburg, 2016. Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, and Andreas Podelski. Fairness modulo theory: A new approach to LTL software model checking. In International Conference on Computer Aided Verification, pages 49–66. Springer, 2015. Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In International Conference on Computer Aided Verification, pages 53–65. Springer, 2001. Rob Gerth, Doron Peled, Moshe Y Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In International Conference on Protocol Specification, Testing and Verification, pages 3–18. Springer, 1995. Gerard J. Holzmann. The model checker SPIN. IEEE Transactions on software engineering, 23(5):279–295, 1997. Gerard J. Holzmann. The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, 2004. Gerard J Holzmann. Explicit-state model checking. In Handbook of Model Checking, pages 153–171. Springer, 2018. Gerard J Holzmann and Doron Peled. An improvement in formal verification. In Formal Description Techniques VII, pages 197–211. Springer, 1995. Gerard J Holzmann, Doron A Peled, and Mihalis Yannakakis. On nested depth first search. The Spin Verification System, 32:23–32, 1996. Saul Kripke. Semantical considerations of the modal logic. Studia Philosophica, 1, 2007. Akash Lal and Shaz Qadeer. Reachability modulo theories. In International Workshop on Reachability Problems, pages 23–44. Springer, 2013. Hong-Yang Lin. Tool support for automata-based model checking of multithreaded programs. Master’s thesis, National Taiwan University, Jan 2021. Kenneth L McMillan. Symbolic model checking. In Symbolic Model Checking, pages 25–60. Springer, 1993. Moshe Y Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322–331. IEEE Computer Society, 1986. | - |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/83194 | - |
| dc.description.abstract | 模型檢測是一種用於驗證程式正確性的全自動方法，這對於軟體安全至關重要。最常用的方法之一是顯式狀態模型檢測。它可以使用各類深度優先搜索演算法來執行，被廣泛用於驗證可以用線性時序邏輯描述的屬性。若程式不正確，驗證期間將會回報違背被驗證屬性的程式執行行為。由於多執行緒程式在實務中非常普遍，因此可以驗證多執行緒程式屬性的模型檢測工具非常有價值。 在本論文中，我們構建了一個名為SCANTU的可擴展模型檢測工具，它具有用於驗證多執行緒C語言程式的可視化用戶界面。我們的工具建立在插件導向的ULTIMATE程式分析框架之上，該框架具有構建可擴展應用程式的良好架構。我們為用戶提供便利的方法來使用由ULTIMATE開發人員構建的插件擴展SCANTU。例如，擴展後，SCANTU用戶可以通過我們的用戶界面執行其他開發者設計的模型檢測演算法。這賦予了SCANTU工具箱的特性，允許用戶將自己需要的插件作為工具添加到SCANTU中，並根據情況選擇合適的工具。隨著ULTIMATE開發人員實作的模型檢測演算法越來越多，用戶可以使用我們的工具輕鬆比較不同演算法之間的執行效率。SCANTU還提供了基本的嵌套深度優先搜索(NDFS)演算法和幾種優化技術來提高效率。我們在論文中展示了我們工具的測試結果，包括多執行緒系統公平性的影響以及我們優化技術的性能。 | zh_TW |
| dc.description.abstract | Model checking is a fully automatic method for verifying the correctness of a program, which is essential for software safety. One of the most commonly used approaches is explicit-state model checking. It may be carried out using variants of depth-first search and is widely adopted to verify properties that can be described in linear temporal logic. An error trace if existing will be found during the verification. As multithreaded programs are very common in practice, model checking tools that can verify the properties of multithreaded programs are valuable. In this thesis, we build an extensible model checking tool called SCANTU with a visual user interface for multithreaded C programs. Our tool is built on the plugin-based ULTIMATE program analysis framework, which has a good architecture for building extensible applications. We provide convenient methods for users to extend SCANTU with plugins constructed by ULTIMATE developers. For example, after extension, SCANTU users can execute model checking algorithms designed by other developers through our user interface. This gives our tool characteristics of a toolbox, allowing users to add the plugins they need as tools to SCANTU, and select the appropriate tools according to the situation. As more model checking algorithms are implemented by ULTIMATE developers, users can easily compare the execution efficiencies between different algorithms with our tool. SCANTU also provides the basic nested depth-first search (NDFS) algorithm and several optimization techniques to improve its efficiency. We present in the thesis the test results of our tool, including the effect of fairness conditions and the performance of our optimization techniques. | en |
| dc.description.provenance | Submitted by admin ntu (admin@lib.ntu.edu.tw) on 2023-01-10T17:15:23Z No. of bitstreams: 0 | en |
| dc.description.provenance | Made available in DSpace on 2023-01-10T17:15:23Z (GMT). No. of bitstreams: 0 | en |
| dc.description.tableofcontents | 摘要 i THESIS ABSTRACT ii 1 Introduction 1 1.1 Background 1 1.2 Motivation and Objectives 2 1.3 Thesis Outline 3 2 Related Works 5 2.1 Explicit-State Model Checking 5 2.2 Symbolic Model Checking 6 2.3 Existing Model Checkers 6 2.3.1 SPIN 6 2.3.2 DIVINE 7 2.3.3 NuSMV 7 2.3.4 ULTIMATE LTLAutomizer 8 3 Preliminaries 9 3.1 Automata-Based Model Checking 9 3.1.1 ω-Automata 9 3.1.2 Kripke Structure 10 3.1.3 Linear Temporal Logic 11 3.1.4 Model Checking Problem 12 3.2 Nested Depth-First Search Algorithm 13 4 Design and Implementation 16 4.1 ULTIMATE Program Analysis Framework 16 4.1.1 Library-ModelCheckerAssistant 17 4.2 Eclipse RCP Application 18 4.3 SCANTU Design and Implementation 20 4.3.1 User Interface 20 4.3.2 Program Design 22 4.3.3 Extension Method 25 4.4 Implementation Techniques 27 4.4.1 Partial Order Reduction for SCANTU 27 4.4.2 Support for Shared Code 32 4.4.3 Optimization of StateSpace Data Structure 33 4.4.4 Fair Cycle Detection 33 5 Experimental Results 36 5.1 Fairness Condition and Property Correctness 37 5.1.1 Enforcing Fairness 37 5.1.2 Correctness Test 41 5.1.3 N Processes Program Test 45 5.2 Performance of Optimization Techniques 50 6 Conclusion 53 6.1 Contributions 53 6.2 Future Works 54 References 56 List of Figures 4.1 An example of an Ultimate toolchain 17 4.2 The structure of an Eclipse RCP application 19 4.3 The user interface of SCANTU 20 4.4 Features now supported by SCANTU 21 4.5 The code before and after code beautification 22 4.6 Annotation Dialog 23 4.7 An example of an Ultimate toolchain file 26 4.8 The expanded asynchronous product of Algorithm 3 28 4.9 The RCFG of Algorithm 3 29 5.1 Result of SCANTU executing Example 1 38 5.2 Result of SCANTU executing Example 2 40 5.3 Result of SCANTU executing Example 1 with fairness detection of acceptance cycles 41 5.4 Result of SCANTU executing Example 2 with wrong LTL Property 42 5.5 Result of SCANTU executing Example 1-Ex 43 5.6 Result of SCANTU executing Example 2-Ex 45 5.7 Result of SCANTU executing Example 3 47 5.8 Result of SCANTU executing Example 4 49 5.9 Executing time result of executing Example 5 51 List of Tables 5.1 Difference in execution time results for Example 1 using fairness checks 41 5.2 Difference in execution time results for Example 3 using fairness checks 50 5.3 Executing time result of executing Example 5 50 5.4 Executing time comparison of Example 4 52 5.5 Executing time comparison of Example 5 52 | - |
| dc.language.iso | en | - |
| dc.subject | 多執行緒程式 | zh_TW |
| dc.subject | 軟體驗證 | zh_TW |
| dc.subject | 偏序縮減 | zh_TW |
| dc.subject | Büchi自動機 | zh_TW |
| dc.subject | 線性時序邏輯 | zh_TW |
| dc.subject | 模型檢測 | zh_TW |
| dc.subject | Software Verification | en |
| dc.subject | Multithreaded Programs | en |
| dc.subject | Partial Order Reduction | en |
| dc.subject | Linear Temporal Logic | en |
| dc.subject | Büchi Automata | en |
| dc.subject | Model Checking | en |
| dc.title | 多執行緒C語言程式的可擴展模型檢測工具 | zh_TW |
| dc.title | An Extensible Model Checker for Multithreaded C Programs | en |
| dc.title.alternative | An Extensible Model Checker for Multithreaded C Programs | - |
| dc.type | Thesis | - |
| dc.date.schoolyear | 111-1 | - |
| dc.description.degree | 碩士 | - |
| dc.contributor.oralexamcommittee | 郁方;陳郁方 | zh_TW |
| dc.contributor.oralexamcommittee | Fang Yu;Yu-Fang Chen | en |
| dc.subject.keyword | Büchi自動機,線性時序邏輯,模型檢測,多執行緒程式,偏序縮減,軟體驗證, | zh_TW |
| dc.subject.keyword | Büchi Automata,Linear Temporal Logic,Model Checking,Multithreaded Programs,Partial Order Reduction,Software Verification, | en |
| dc.relation.page | 57 | - |
| dc.identifier.doi | 10.6342/NTU202204271 | - |
| dc.rights.note | 同意授權(全球公開) | - |
| dc.date.accepted | 2022-10-12 | - |
| dc.contributor.author-college | 管理學院 | - |
| dc.contributor.author-dept | 資訊管理學系 | - |
| 顯示於系所單位： | 資訊管理學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| U0001-1110202213421100.pdf | 1.12 MB | Adobe PDF | 檢視/開啟 |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。