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

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:張子建
研究生(外文):Tzu-Chien Chang
論文名稱:針對以自動機為基礎之驗證而設計的PSL公式轉譯
論文名稱(外文):Translation of PSL Formulae for Automata-Based Verification
指導教授:蔡益坤
指導教授(外文):Yih-Kuen Tsay
口試委員:郁方陳郁方
口試委員(外文):Fang YuYu-Fang Chen
口試日期:2020-07-28
學位類別:碩士
校院名稱:國立臺灣大學
系所名稱:資訊管理學研究所
學門:電算機學門
學類:電算機一般學類
論文種類:學術論文
論文出版年:2020
畢業學年度:108
語文別:英文
論文頁數:49
中文關鍵詞:Büchi 自動機公式轉譯GOAL模型檢驗屬性規範語言時序邏輯驗證
外文關鍵詞:Büchi AutomataFormula TranslationGOALModel CheckingProperty Specification LanguageTemporal LogicVerification
DOI:10.6342/NTU202002437
相關次數:
  • 被引用被引用:0
  • 點閱點閱:48
  • 評分評分:
  • 下載下載:0
  • 收藏至我的研究室書目清單書目收藏:0
在現今電腦硬體業界,搭配邏輯屬性規範並以自動機為基礎的模型檢驗已經成為一種常用的偵測設計錯誤技術。為便於撰寫此類邏輯規範,屬性規範語言(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。
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.
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
[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.
電子全文 電子全文(網際網路公開日期:20230801)
連結至畢業學校之論文網頁點我開啟連結
註: 此連結為研究生畢業學校所提供,不一定有電子全文可供下載,若連結有誤,請點選上方之〝勘誤回報〞功能,我們會盡快修正,謝謝!
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top