https://scholars.lib.ntu.edu.tw/handle/123456789/152174
Title: | 混合系統的全符號式自動化分析軟體工具環境(2/3) Environment for Symbolic Automation Verification Tool of Hybrid |
Authors: | 王凡 | Issue Date: | 31-Jul-2004 | Publisher: | 臺北市:國立臺灣大學電機工程學系暨研究所 | Abstract: | 我們藉著國科會三年長期的支持,我 們得以深入研究及發展驗證工具軟體RED, 透過定義一種新的時態邏輯TECTLf,在驗 證上獲得了更大的彈性,而能夠包含狀 態、事件和公平的假設。配合這種邏輯, 衍生出對應的演算法,亦能實現模型驗證 之目的,最後再將此一功能,整合到RED之 中,成為5.1的版本。 With the three-year support from NSC, we aim at developing the verification tool : RED (Region-Encoding Diagram). At this moment, there lacks a specification language for distributed real-time system properties involving states and events. There also lacks a language for fairness assumptions in dense-time systems. We have defined a new temporal logic, TECTLf, for the flexible specification of distributed real-time systems with constraints involving events, states, and fairness assumptions. Then we have also designed algorithms for model-checking TECTLf formulas. Finally, we have endeavored to implement and experiment the ideas in our tool, RED 5.1. |
URI: | http://ntur.lib.ntu.edu.tw//handle/246246/7994 | Other Identifiers: | 922213E002104 | Rights: | 國立臺灣大學電機工程學系暨研究所 |
Appears in Collections: | 電機工程學系 |
File | Description | Size | Format | |
---|---|---|---|---|
922213E002104.pdf | 129.01 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.