請用此 Handle URI 來引用此文件：
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53518完整後設資料紀錄
| DC 欄位 | 值 | 語言 |
|---|---|---|
| dc.contributor.advisor | 蔡益坤(Yih-Kuen Tsay) | |
| dc.contributor.author | Tzu-Chien Chang | en |
| dc.contributor.author | 張子建 | zh_TW |
| dc.date.accessioned | 2021-06-16T02:25:19Z | - |
| dc.date.available | 2023-08-01 | |
| dc.date.copyright | 2020-08-20 | |
| dc.date.issued | 2020 | |
| dc.date.submitted | 2020-08-17 | |
| dc.identifier.citation | [1] D. Basin, V. Jugè, F. Klaedtke, and E. Zălinescu. Enforceable security policies revisited. ACM Transactions on Information and System Security, 16(1), June 2013. [2] I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, and Y. Rodeh. The temporal logic Sugar. In Proceedings of the 13rd International Conference on Computer Aided Verification (CAV ’01), LNCS 2102, 2001. [3] S. Ben-David, R. Bloem, D. Fisman, A. Griesmayer, I. Pill, and S. Ruah. Automata construction algorithms optimized for PSL. Technical Report FP6-IST-507219, PROSYD, 2005. [4] 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. [5] D. Bustan, D. Fisman, and J. Havlicek. Automata Construction for PSL. Technical Report MCS05-04, The Weizmann Institute of Science, 2005. [6] J.-S. Chang. A comprehensive comparison of temporal formula to automaton translation algorithms. Master’s thesis, Department of Information Management, National Taiwan University, November 2009. [7] Y.-W. Chang. Transformation and classification of temporal properties with applications. Master’s thesis, Department of Information Management, National Taiwan University, July 2010. [8] Y. Choueka. Theories of automata on ω-tapes: A simplified approach. Journal of Computer and System Science, 8:117–141, 1974. [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] A. Cimatti, M. Roveri, S. Semprini, and S. Tonetta. From PSL to NBA: a modular symbolic encoding. In Proceedings of the Formal Methods in Computer Aided Design, 2006. [11] E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. The MIT Press, 1999. [12] M. Daniele, F. Giunchiglia, and M.Y. Vardi. Improved automata generation for linear temporal logic. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV ’99), LNCS 1633, pages 249–260. Springer, 1999. [13] C. Dax, F. Klaedtke, and M. Lange. On regular temporal logics with past. In Proceedings of the 36th International Colloqium on Automata, Languages, and Programming (ICALP ’09), LNCS 5556, pages 175–187. Springer-Verlag, July 2009. [14] G. De Giacomo and M.Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI ’13), pages 854–860. AAAI Press, August 2013. [15] A. Duret-Lutz, A. Lewkowicz, A. Fauchille, T. Michaud, E. Renault, and L. Xu. Spot 2.0 – a framework for LTL and ω-automata manipulation. In Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA ’16), LNCS 9938, pages 122–129, October 2016. [16] A. Duret-Lutz and D. Poitrenaud. SPOT: An extensible model checking library using transition-based generalized Büchi automata. In Proceedings of the 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS ’04), pages 76–83. IEEE Computer Society, 2004. [17] C. Eisner and D. Fisman. A Practical Introduction to PSL. Springer, Boston, MA, 2006. [18] C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. McIssac, and D.V. Campenhout. Reasoning with temporal logic on truncated paths. In Proceedings of 15th International Conference on Computer-Aided Verification (CAV ’03), LNCS 2725, pages 27–39. Springer, 2003. [19] C. Eisner, D. Fisman, J. Havlicek, A. McIssac, and D.V. Campenhout. The definition of a temporal clock operator. In Proceedings of the 30th International Colloqium on Automata, Languages, and Programming (ICALP ’03), LNCS 2719, pages 857–870. Springer-Verlag, July 2003. [20] K. Etessami and G.J. Holzmann. Optimizing Büchi automata. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR ’00), LNCS 1877, pages 153–167. Springer-Verlag, 2000. [21] M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194–211, 1979. [22] P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV ’01), LNCS 2102, pages 53–65. Springer, 2001. [23] R. Gerth, D. Peled, M.Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing, and Verification, pages 3–18. Chapman Hall, 1995. [24] J.G. Henriksen and P.S. Thiagarajan. Dynamic linear time temporal logic. Annals of Pure and Applied logic, 96(1-3):187–207, March 1999. [25] IEEE Computer Society. IEEE Standard for Property Specification Language (PSL). IEEE Std 1850™-2010, 2010. [26] A. Isli. Mapping an LPTL formula into a büchi alternating automaton accepting its models. Technical Report MPI-I-94-230, Max-Planck-Institut für Informatik, 1994. pp.85-90. [27] M. Leucker and C. Sànchez. Regular linear temporal logic. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC ’07), LNCS 4711, pages 291–305. Springer, 2007. [28] S. Miyano and T. Hayashi. Alternating finite automata on omega-words. Theoretical Computer Science, 32:321–330, 1984. [29] D.E. Muller. Infinite sequences and finite machines. In Proceedings of the 4th Annual IEEE Symposium on Foundations of Computer Science (FOCS ’63), pages 3–16, 1963. [30] D.E. Muller, A. Saoudi, and P.E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS ’88), pages 422–427. IEEE Computer Society Press, 1988. [31] V. Pratt. Semantical considerations on Floyd-Hoare logic. In Proceedings of the 17th IEEE Symposium on Foundations of Computer Science, pages 109–121. IEEE Computer Society, 1976. [32] S. Ruah, D. Fisman, and S. Ben-David. Automata construction for on-the-fly model checking PSL safety simple subset. Technical Report H-0234, IBM Haifa Research Lab, 2005. [33] C. Sànchez and M. Leucker. Regular linear temporal logic with past. In Proceedings of the International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI ’10), LNCS 5944, pages 295–311. Springer, 2007. [34] F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV ’00), LNCS 1855, pages 248–263. Springer, 2000. [35] 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. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’08), LNCS 4963, pages 346–350. Springer, 2008. [36] 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. [37] M.Y. Vardi. The rise and fall of LTL. In the 2nd International Symposium on Games, Automata, Logics and Formal Verification (GandALF ’11), 2011. [38] P. Wolper, M.Y. Vardi, and A.P. Sistala. Reasoning about infinite computation paths. In the 24th Annual Symposium on Foundations of Computer Science (FOCS ’83), pages 185–194. Washington: IEEE Computer Society Press, 1983. [39] L. Yu and H.-W. Chen. Method of constructing two-way alternating automata for PSL and translation to nondeterministic automata. Journal of Software, 21(1):34–46, January 2010. | |
| dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/53518 | - |
| dc.description.abstract | 在現今電腦硬體業界，搭配邏輯屬性規範並以自動機為基礎的模型檢驗已經成為一種常用的偵測設計錯誤技術。為便於撰寫此類邏輯規範，屬性規範語言(PSL) 這個相容於主流硬體描述語言(HDL) 的標準因而被設計出來。PSL 結合了正規表達式與線性時序邏輯(LTL)，並藉此獲得了高於兩者的表述力。有關轉譯PSL 公式為自動機的部分，目前已有研究討論特定目的下的應用，也有一些工具支援PSL 特定子集的轉譯。 本篇論文中，我們將選取一個PSL 的子集，並增添詢問建構及一些對偶運算子，使得每一種公式都能得到否定標準式(NNF)。這個極小的子集PSL_D 可以如同標準PSL 一般表述所有ω-正規語言。我們為PSL_D 定義一個歸納式的語意，並以此為基礎提出一個即時處理方法，可將PSL_D 公式轉譯為廣義Büchi 自動機(GBW)。我們以JAVA 實作此方法，並做為擴充整合到可操作ω-自動機和邏輯公式的圖像化工具GOAL。我們手動挑選具代表性的PSL 樣式屬性來測試實作的正確性。對於語法上與LTL 相等的PSL_D 公式，我們將其轉譯為GBW，並將結果與現存演算法(如LTL2BA)的轉譯結果作比較；對於其他類型，我們準備數種以不同形式編碼的公式，從中挑選語意相等者，將它們轉譯為GBW，再相互進行等價測試。此種轉譯出的自動機可以馬上引入常規驗證程序運用。有了此轉譯法的協助，使用者能更得心應手的在不同業界與學界場合利用GOAL。 | zh_TW |
| dc.description.abstract | Automata-based model checking with logical properties specification as a technique for detecting design errors is now well established in the hardware industry. For the ease of writing such specifications, the standard Property Specification Language (PSL) has been designed to be compatible with mainstream Hardware Description Languages (HDLs). PSL combines regular expressions and Linear Temporal Logic (LTL) to attain stronger expressive power than both of them. Regarding translation of PSL formulae to automata, there have been researches focusing on applications for specialized purposes. Several publicly available tools support translation of specific subsets of PSL formulae. In this thesis, we select a subset of the standard PSL and enrich it with queries and dual operators so that every formula can have a Negation Normal Form (NNF). This minimal subset, denoted PSL_D, can describe all ω-regular languages like standard PSL. We define an inductive semantics for PSL_D and present an on-the-fly approach based on it to translating PSL_D formulae to generalized Büchi word automata (GBW). We implement the approach in Java and integrate it into GOAL, a graphic tool for manipulating omega-automata and logic formulae, as an extension. We manually select representative PSL-style properties for testing correctness of the implementation. For PSL_D formulae that are syntactically LTL, we translate them to GBW and compare them against automata translated by existing algorithms like LTL2BA. For other cases, we prepare formulae encoded in different forms, pick congruent cases, translate them to GBW, and do equivalence test between them. The translated automata can immediately be introduced into common operations of validation and verification. With the support of this translation, users can better utilize GOAL in various industrial and academic settings. | en |
| dc.description.provenance | Made available in DSpace on 2021-06-16T02:25:19Z (GMT). No. of bitstreams: 1 U0001-0508202010460900.pdf: 1542856 bytes, checksum: 4b9f8f06b8108c2f67464d3f669e7faf (MD5) Previous issue date: 2020 | en |
| dc.description.tableofcontents | 1 Introduction 1 1.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.1.1 Logic to Automata . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.1.2 LTL to Automata with Optimization . . . . . . . . . . . . . . . . 2 1.1.3 Translation From PSL to Automata . . . . . . . . . . . . . . . . 3 1.1.4 Existing tools supporting PSL specification for model checking . . 3 1.2 Motivation and Objectives . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Thesis outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2 Preliminaries 5 2.1 Symbols, Words, and Languages . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Automata on Finite Words . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3 Automata on Infinite Words . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3.1 ω-automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3.2 Nondeterministic Büchi Word Automata (NBW) . . . . . . . . . 7 2.3.3 Generalized Büchi Word Automata (GBW) . . . . . . . . . . . . 9 3 Related Works 10 3.1 Before PSL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Property Specification Language (PSL) . . . . . . . . . . . . . . . . . . . 11 3.2.1 Lexical Structures . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2.2 Word Length and Views . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.3 The Simple Subset . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2.4 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2.5 Unclocked Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.3 Linear Dynamic Logic (LDL) . . . . . . . . . . . . . . . . . . . . . . . . 17 3.4 Tools related to PSL translations . . . . . . . . . . . . . . . . . . . . . . 19 3.4.1 LTL2BA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.4.2 NuSMV . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.4.3 PSL2BA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.4.4 SPOT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.4.5 GOAL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4 A PSL Subset and Its Translation 23 4.1 The Subset Language PSLD . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.1.1 Unclocked PSLD Syntax . . . . . . . . . . . . . . . . . . . . . . . 24 4.1.2 Unclocked PSLD Semantics . . . . . . . . . . . . . . . . . . . . . 24 4.1.3 Expressive Power . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 4.2 Automata Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 4.2.1 NNF Rewriting . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.2.2 The Data Structure . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.2.3 The Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.3 A Live Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5 Implementation and Experiments 41 5.1 Base . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 5.2 Environment and Implementation . . . . . . . . . . . . . . . . . . . . . . 42 5.3 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 6 Conclusion 44 6.1 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 6.1.1 A subset PSLD of standard PSL . . . . . . . . . . . . . . . . . . . 44 6.1.2 A translation algorithm from PSLD formulae to GBW . . . . . . 44 6.1.3 Integration to GOAL . . . . . . . . . . . . . . . . . . . . . . . . . 44 6.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 6.2.1 Extend support to full standard PSL . . . . . . . . . . . . . . . . 45 6.2.2 Collect classic PSL formulae as test cases . . . . . . . . . . . . . 45 6.2.3 Develop other translation approaches . . . . . . . . . . . . . . . . 45 6.2.4 Improve the current on-the-fly algorithm . . . . . . . . . . . . . . 45 References 46 | |
| dc.language.iso | en | |
| dc.title | 針對以自動機為基礎之驗證而設計的PSL公式轉譯 | zh_TW |
| dc.title | Translation of PSL Formulae for Automata-Based Verification | en |
| dc.type | Thesis | |
| dc.date.schoolyear | 108-2 | |
| dc.description.degree | 碩士 | |
| dc.contributor.author-orcid | 0000-0002-3446-5151 | |
| dc.contributor.advisor-orcid | 蔡益坤(0000-0002-5960-1615) | |
| dc.contributor.oralexamcommittee | 郁方(Fang Yu),陳郁方(Yu-Fang Chen) | |
| dc.subject.keyword | Büchi 自動機,公式轉譯,GOAL,模型檢驗,屬性規範語言,時序邏輯,驗證, | zh_TW |
| dc.subject.keyword | Büchi Automata,Formula Translation,GOAL,Model Checking,Property Specification Language,Temporal Logic,Verification, | en |
| dc.relation.page | 49 | |
| dc.identifier.doi | 10.6342/NTU202002437 | |
| dc.rights.note | 有償授權 | |
| dc.date.accepted | 2020-08-17 | |
| dc.contributor.author-college | 管理學院 | zh_TW |
| dc.contributor.author-dept | 資訊管理學研究所 | zh_TW |
| 顯示於系所單位： | 資訊管理學系 | |
文件中的檔案：
| 檔案 | 大小 | 格式 | |
|---|---|---|---|
| U0001-0508202010460900.pdf 目前未授權公開取用 | 1.51 MB | Adobe PDF |
系統中的文件，除了特別指名其著作權條款之外，均受到著作權保護，並且保留所有的權利。