請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/80689完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 蔡益坤(Yih-Kuen Tsay) | |
| dc.contributor.author | Hong-Yang Lin | en |
| dc.contributor.author | 林宏陽 | zh_TW |
| dc.date.accessioned | 2022-11-24T03:12:59Z | - |
| dc.date.available | 2021-11-05 | |
| dc.date.available | 2022-11-24T03:12:59Z | - |
| dc.date.copyright | 2021-11-05 | |
| dc.date.issued | 2021 | |
| dc.date.submitted | 2021-10-20 | |
| dc.identifier.citation | Rajeev Alur and Parthasarathy Madhusudan. Adding nesting structure to words. Journal of the ACM (JACM), 56(3):1–43, 2009. Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, and Vladimír Štill. Model checking of C and C++ with DIVINE 4. In International Symposium on Automated Technology for Verification and Analysis, pages 201–207. Springer, 2017. Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C specification. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 193–207. Springer, 1999. Randal E. Bryant. Graph-based algorithms for boolean function manipulation. Computers, IEEE Transactions on, 100(8):677–691, 1986. J. Richard Büchi. On a decision method in restricted second order arithmetic. In The Collected Works of J. Richard Büchi, pages 425–435. Springer, 1990. J.R. Büchi. On a decision method in restricted second-order arithmetic. In Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, pages 1–11, 1962. Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and Lain-Jinn Hwang. Symbolic model checking: 10^20 states and beyond. Information and Computation, 98(2):142–170, 1992. Yaacov Choueka. Theories of automata on ω-tapes: A simplified approach. Journal of Computer and System Sciences, 8(2):117–141, 1974. Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV 2: An opensource tool for symbolic model checking. In International Conference on Computer Aided Verification, pages 359–364. Springer, 2002. Alessandro Cimatti, Edmund Clarke, Fausto Giunchiglia, and Marco Roveri. NuSMV: A new symbolic model verifier. In International Conference on Computer Aided Verification, pages 495–499. Springer, 1999. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, 1999. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C. In International Conference on Software Engineering and Formal Methods, pages 233–247. Springer, 2012. Martin De Wulf, Laurent Doyen, Nicolas Maquet, and J.-F. Raskin. Antichains: Alternative algorithms for LTL satisfiability and modelchecking. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 63–77. Springer, 2008. Daniel Dietsch. Automated verification of system requirements and software specifications. PhD thesis, University of Freiburg, Freiburg im Breisgau, Germany, 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. Carsten Fritz. Concepts of automata construction from LTL. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 728–742. Springer, 2005. Paul Gastin and Denis Oddoux. Fast LTL to Büchi automata translation. In International Conference on Computer Aided Verification, pages 53–65. Springer, 2001. Patrice Godefroid. Using partial orders to improve automatic verification methods. In International Conference on Computer Aided Verification, pages 176–185. Springer, 1990. Klaus Havelund and Thomas Pressburger. Model checking JAVA programs using JAVA pathfinder. International Journal on Software Tools for Technology Transfer, 2(4):366–381, 2000. Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler, et al. Ultimate Automizer and the search for perfect interpolants. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 447–451. Springer, 2018. Matthias Heizmann, Jürgen Christ, Daniel Dietsch, Evren Ermis, Jochen Hoenicke, Markus Lindenmann, Alexander Nutz, Christian Schilling, and Andreas Podelski. Ultimate Automizer with SMTInterpol. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 641–643. Springer, 2013. Matthias Heizmann, Daniel Dietsch, Marius Greitschus, Jan Leike, Betim Musa, Claus Schätzle, and Andreas Podelski. Ultimate Automizer with two-track proofs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 950–953. Springer, 2016. Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, and Andreas Podelski. Ultimate Automizer with array interpolation. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 455–457. Springer, 2015. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Refinement of trace abstraction. In International Static Analysis Symposium, pages 69–85. Springer, 2009. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. Nested interpolants. ACM Sigplan Notices, 45(1):471–482, 2010. G. J. Holzmann. The model checker spin. IEEE Transactions on Software Engineering, 23(5), 1997. Gerard J. Holzmann. An improved protocol reachability analysis technique. Software: Practice and Experience, 18(2):137–161, 1988. Gerard J. Holzmann. State compression in SPIN: Recursive indexing and compression training runs. In Proceedings of Third International Spin Workshop, 1997. 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:81–89, 1996. Gerard J. Holzmann and Anuj Puri. A minimized automaton representation of reachable states. International Journal on Software Tools for Technology Transfer, 2(3):270–278, 1999. G.J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2003. ISO. ISO/IEC 9899:2011 Information technology — Programming languages — C. International Organization for Standardization, Geneva, Switzerland, December 2011. Saul Kripke. Semantical considerations of the modal logic. 2007. O. Kupferman and M.Y. Vardi. An automata-theoretic approach to modular model checking. ACM Transactions on Programming Languages and Systems, 22(1):87–128, January 2000. Akash Lal and Shaz Qadeer. Reachability modulo theories. In International Workshop on Reachability Problems, pages 23–44. Springer, 2013. K. Rustan M. Leino. This is Boogie 2. manuscript KRML, 178(131):9, 2008. Kenneth L. McMillan. The SMV system. In Symbolic Model Checking, pages 61–85. Springer, 1993. Satoru Miyano and Takeshi Hayashi. Alternating finite automata on ω-words. Theoretical Computer Science, 32(3):321–330, 1984. D.E. Muller. Infinite sequences and finite machines. In Proceedings of the 4th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1963), pages 3–16, 1963. Doron Peled. Combining partial order reductions with on-the-fly modelchecking. In International Conference on Computer Aided Verification, pages 377–390. Springer, 1994. A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45–60, 1981. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pages 46–57. IEEE, 1977. Thomas Reps, Susan Horwitz, and Mooly Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 49–61, 1995. Robert Tarjan. Depth-first search and linear graph algorithms. SIAM journal on computing, 1(2):146–160, 1972. Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, W.-C. Chan, and C.-J. Luo. GOAL extended: Towards a research tool for omega-automata and temporal logic. pages 346–350. Springer, 2008. Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, W.-C. Chan, C.-J. Luo, and J.-S. Chang. Tool support for learning Büchi automata and linear temporal logic. Formal Aspects of Computing, 21(3):259–275, 2009. Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for concurrency, pages 238–266. Springer, 1996. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/80689 | - |
| dc.description.abstract | 基於自動機的時序邏輯模型驗證牽涉到兩個Büchi自動機，一個代表被驗證系統的行為，另一個描述違背時序規範的行為。如果系統違反給定的性質，則在由系統自動機和性質自動機所構成的同步乘積中存在一個套索狀的路徑。當系統中有平行運行的程序時，系統自動機由多個程序的自動機的不同步乘積構成，代表輸入的多執行緒程式的交錯執行，每個自動機代表一個執行緒。有鑑於包含全部交錯執行的全域狀態空間過分地龐大，必須運用偏序縮減，在保留正確性的同時生成精簡的狀態空間。 這篇論文旨在創立一個便利基於自動機的多執行緒程式模型驗證實作的函式庫。這個函式庫建立在Ultimate程式分析框架中，它包含一個主要的類別，可用來接受控制流程圖和由現有部件生成的性質自動機。此主要類別提供基礎的模型驗證方法，包括從控制流程圖即時生成系統狀態、特定狀態對外轉移的可行性檢查以及實際執行一個選定的轉移。其中也包含偏序縮減的一個重要步驟：基於安全度的程序重新排序方法。在Ultimate的模組化架構下，輸入的程式和規格被轉譯成中間語言Boogie，因此隨後的分析能脫離輸入語言特定語法的限制。我們的工具支援為多執行緒程式全域狀態空間的即時探索打下基礎，不同的基於自動機模型驗證演算法因此能被方便地實作出來。 | zh_TW |
| dc.description.provenance | Made available in DSpace on 2022-11-24T03:12:59Z (GMT). No. of bitstreams: 1 U0001-1810202119524700.pdf: 731898 bytes, checksum: 00c814c0e92b00b3d2f2499965d77444 (MD5) Previous issue date: 2021 | 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 4 2.1 Existing Model Checkers . . . . . . . . . . . . . . . . . . . . 4 2.1.1 SPIN . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.2 NuSMV . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.3 DIVINE . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.4 Java PathFinder . . . . . . . . . . . . . . . . . . . 7 2.1.5 Ultimate . . . . . . . . . . . . . . . . . . . . . . . 7 2.1.6 Frama-C . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2 Other Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.1 LTL2BA . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.2 GOAL . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3 Preliminaries 11 3.1 Automata Theory . . . . . . . . . . . . . . . . . . . . . . . . 11 3.1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . 11 3.1.2 Automata on Finite Words . . . . . . . . . . . . . . 11 3.1.3 Automata on Infinite Words . . . . . . . . . . . . . . 12 3.1.4 Variants of Büchi Automata . . . . . . . . . . . . . . 14 3.1.5 Miyano-Hayashi Construction . . . . . . . . . . . . . 16 3.2 Kripke Structure . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 Temporal Logic . . . . . . . . . . . . . . . . . . . . . . . . . 18 3.3.1 Linear Temporal Logic (LTL) . . . . . . . . . . . . . 18 3.4 Model-Checking Problem . . . . . . . . . . . . . . . . . . . . 20 3.4.1 Products of Automata . . . . . . . . . . . . . . . . . 21 3.5 Model-Checking Algorithms . . . . . . . . . . . . . . . . . . 22 3.5.1 Nested Depth First Search (NDFS) . . . . . . . . . . 22 3.6 Partial Order Reduction . . . . . . . . . . . . . . . . . . . . 23 4 Design and Implementation 30 4.1 Software Architecture . . . . . . . . . . . . . . . . . . . . . 30 4.1.1 Ultimate’s Framwork . . . . . . . . . . . . . . . . . 32 4.1.2 Ultimate’s Intermediate Verification Language . . . 36 4.1.3 Recursive Control Flow Graph . . . . . . . . . . . . 36 4.2 Design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.2.1 Class Design . . . . . . . . . . . . . . . . . . . . . . 38 4.3 Implementation and Optimization Techniques . . . . . . . . 42 4.3.1 APIs . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.3.2 Array Handling . . . . . . . . . . . . . . . . . . . . . 47 4.3.3 Support for Multithreaded Programs . . . . . . . . . 49 4.3.4 Techniques . . . . . . . . . . . . . . . . . . . . . . . 49 4.3.5 Comparison with Spin . . . . . . . . . . . . . . . . . 50 5 Examples 52 5.1 Increment Using a Recursive Function . . . . . . . . . . . . 52 5.2 Multithreaded Programs . . . . . . . . . . . . . . . . . . . . 58 5.2.1 Fork Handling . . . . . . . . . . . . . . . . . . . . . 61 5.2.2 Join Handling . . . . . . . . . . . . . . . . . . . . . . 61 6 Conclusion 63 6.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . 63 6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . 64 Appendix A Boogie programs 67 References 72 | |
| 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 | Büchi Automata | en |
| dc.subject | Linear Temporal Logic | en |
| dc.subject | Model Checking | en |
| dc.subject | Multithreaded Programs | en |
| dc.subject | Partial Order Reduction | en |
| dc.title | 基於自動機的多執行緒程式模型驗證工具支援 | zh_TW |
| dc.title | Tool Support for Automata-Based Model Checking of Multithreaded Programs | en |
| dc.date.schoolyear | 109-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.oralexamcommittee | 陳郁方(Hsin-Tsai Liu),郁方(Chih-Yang Tseng) | |
| 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 | 76 | |
| dc.identifier.doi | 10.6342/NTU202103842 | |
| dc.rights.note | 同意授權(限校園內公開) | |
| dc.date.accepted | 2021-10-20 | |
| dc.contributor.author-college | 管理學院 | zh_TW |
| dc.contributor.author-dept | 資訊管理學研究所 | zh_TW |
| 顯示於系所單位： | 資訊管理學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| U0001-1810202119524700.pdf 授權僅限NTU校內IP使用（校園外請利用VPN校外連線服務） | 714.74 kB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。