https://scholars.lib.ntu.edu.tw/handle/123456789/152174
標題: | 混合系統的全符號式自動化分析軟體工具環境(2/3) Environment for Symbolic Automation Verification Tool of Hybrid |
作者: | 王凡 | 公開日期: | 31-七月-2004 | 出版社: | 臺北市:國立臺灣大學電機工程學系暨研究所 | 摘要: | 我們藉著國科會三年長期的支持,我 們得以深入研究及發展驗證工具軟體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 | 其他識別: | 922213E002104 | Rights: | 國立臺灣大學電機工程學系暨研究所 |
顯示於: | 電機工程學系 |
檔案 | 描述 | 大小 | 格式 | |
---|---|---|---|---|
922213E002104.pdf | 129.01 kB | Adobe PDF | 檢視/開啟 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。