國立臺灣大學電機工程學系暨研究所王凡2006-07-252018-07-062006-07-252018-07-062004-07-31http://ntur.lib.ntu.edu.tw//handle/246246/7993感謝國科會三年的長期支持，我們更 深入發展能將數學模型、問題分析、邏輯 驗證等相關技術加以結合，而開發出的軟 體工具RED。除了利用功能強大的資料結 構有效節省許多空間與時間，並可自動進 行高效率複雜即時系統驗證之外，對其底 層的基礎技術，更加入了涵蓋率的應用， 以預測執行效能，找出合適乃至最佳化的 驗證方式，向自動化驗證邁進了一大步， 亦提高在業界實務上的應用價值。Thanks to the support of National Science Council for the long-term support of three years, we were able to develop the fundamental technologies of the verification tool, RED ( Region-Encoding Diagram ). By using new data-structures, analysis techniques, and verification techniques, this tool can carry out efficient state-space representation and manipulations. Besides, we add the application of coverage estimation in the tool to predict the performance and efficiency of strategies. According the data , we can find the best or the adaptive methods to execute. We improve the applicability and value of RED in industry.application/pdf296444 bytesapplication/pdfzh-TW國立臺灣大學電機工程學系暨研究所即時系統驗證涵蓋率模型 檢驗全符號式模擬Real-time systemverificationcoveragemodel checkingsymbolic simulation即時系統全符號式驗證工具的底層基礎技術（3/3）Fundamental Technologies for Verification Tool of Real-Time Systemreporthttp://ntur.lib.ntu.edu.tw/bitstream/246246/7993/1/922213E002103.pdf