針對以自動機為基礎之驗證而設計的PSL公式轉譯

Translation of PSL Formulae for Automata-Based Verification

張子建(Tzu-Chien Chang)

指導教授 ： 蔡益坤

國立臺灣大學/管理學院/資訊管理學研究所/碩士(2020年)

https://doi.org/10.6342/NTU202002437

摘要

在現今電腦硬體業界，搭配邏輯屬性規範並以自動機為基礎的模型檢驗已經成為一種常用的偵測設計錯誤技術。為便於撰寫此類邏輯規範，屬性規範語言(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。

關鍵字

Büchi 自動機 ； 公式轉譯 ； 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.

並列關鍵字

Büchi Automata ； Formula Translation ； GOAL ； Model Checking ； Property Specification Language ； Temporal Logic ； Verification

參考文獻

[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.