https://scholars.lib.ntu.edu.tw/handle/123456789/105146
Title: | 以時間邏輯為表示法的模組細步化 | Other Titles: | Modular Refinement in Temporal Logic | Authors: | 蔡益坤 | Keywords: | 假設/保證;組合式驗證;並行系統;分解;模組細步化;模組化驗證;PVS;細步化;規格;時間邏輯;驗證;Assumption-Guarantee;Compositional Verification;Concurrent Systems;Decomposition;Modular Refinement;Modular Verification;Refinement;Specification;Temporal Logic;Verification | Issue Date: | 2001 | Publisher: | 臺北市:國立臺灣大學資訊管理學系暨研究所 | Abstract: | 開發大型系統時,我們往往以系統各模 組的抽象規格為開端,然後將各抽象模組逐 漸細步化為具體的、顯然可以實作的模組。 要確保這細步化過程的正確性,我們必須能 夠證明較具體模組所組成的系統確實滿足對 應的較抽象模組所組成的系統的所有性質。 如果有驗證法則能讓我們將這類的驗證需求 化簡為驗證各相對應模組之間的關係,則整 個驗證工作就會變得簡單許多。在本項研究 計畫裡,我們探討如何運用Manna 和Pnueli 所定義的線性時間邏輯(LTL)於確保前述模 組細步化過程的正確性。 Abadi 和Lamport 這兩位研究者對以時 間邏輯為表示法的模組細步化做了開創性的 貢獻,他們所用的TLA 即是時間邏輯的一 種。他們的研究指出假設/保證式規格在模 組細步化中扮演了基礎但隱性的角色。我們 隨後以LTL 為表示法將他們的研究結果做了 一番更清楚的詮釋。本研究之初衷即在利用 LTL 表達能力的長處以獲致更易懂易用的模 組細步化驗證法則。我們的主要研究成果包 含了一個適用於封閉系統的模組細步化驗證 法則,以及一個廣義化、適用於開放系統的 驗證法則;兩者均完全以LTL 的語法表示。 When developing a large system, we typically start with the abstract specifications of its constituent modules and gradually refine the abstract modules into concrete, straightforwardly implementable modules. Correctness of this modular refinement process entails proof obligations of the form that the composition of more concrete modules implements the composition of more abstract modules. The verification task can be made easier if there exist proof rules that offer the possibility of breaking those proof obligations down to the module level. In this research, we investigate the use of linear-time temporal logic, specifically LTL of Manna and Pnueli, in facilitating the aforementioned modular refinement process. Abadi and Lamport pioneered the work on modular refinement with temporal logic. They showed that assumption-guarantee specifications play a fundamental, thought implicit, role in modular refinement. We have subsequently demonstrated the advantage of LTL over TLA, the temporal logic used by Abadi and Lamport, in formulating assumption-guarantee specifications. We set to again take advantage of the expressive power of LTL so as to obtain more easily understandable and usable modular refinement rules. The main results of this work include a modular refinement rule for closed systems and a generalized one for open systems or modules; both are purely syntactical within LTL. |
URI: | http://ntur.lib.ntu.edu.tw//handle/246246/18809 | Other Identifiers: | 892213E002109 | Rights: | 國立臺灣大學資訊管理學系暨研究所 |
Appears in Collections: | 資訊管理學系 |
File | Description | Size | Format | |
---|---|---|---|---|
892213E002109.pdf | 255.2 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.