Please use this identifier to cite or link to this item:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/55095
Title: | 弱硬式系統之正規驗證 Formal Verification of Weakly-Hard Systems |
Authors: | Kai-Chieh Chang 張凱捷 |
Advisor: | 林忠緯(Chung-Wei Lin) |
Keyword: | 弱硬式系統,系統安全驗證,圖論, Weakly-Hard systems,Safety veri cation,Graph theory, |
Publication Year : | 2020 |
Degree: | 碩士 |
Abstract: | 隨著當今系統架構設計複雜度的提升,硬式即時系統要求顯得過於嚴格,於是弱硬式系統的概念便被提出來緩和限制,允許特定數量的死線被錯過。一個弱硬式限制可以由 (m, k) 來描述,表示在連續的k 個事件中,最多只允許有m 個事件錯過對應的死線。這篇論文考慮了兩種不同的系統模型,分別是離散的有限狀態機和連續的動態系統,我們首先提出了建構安全狀態表的方法,其中包含了所有可能的 (m, k),接著展示狀態壓縮的技巧來解決特定的 (m, k),再進一步的使用了分層廣度優先遍歷來有效率的 建構出這張表。此外我們也研究出了方格剖分技巧,將連續的難題轉化為一個離散的圖論問題,安全起始區域便可通過連通性分析來獲得。在實驗結果的部分,我們展現出新算法的效率與正確性,以及對比於一些相關研究的優點。 As hard timing constraints have become pessimistic with the increasing complexity of the system architecture, weakly-hard systems are introduced to relax the constraints by allowing some deadline misses. A weakly-hard constraint can be described as (m; k), meaning that there are at most m instances not meet the deadline among any k task executions. In this thesis, we consider both discrete finite-state machine real-time systems and continuous dynamical systems. We first introduce safety tables consisting of all (m; k) pairs, which can be built with our monotonic approach. Then, we use a mask compression technique to e ciently solve the reachability problem for a single (m; k) and further developed our layered BFS approach to get the results for the entire safety table. We also propose a grid decomposition method and build the reachability relation to nd the safe initial region for the dynamical system with dynamic programming and graph theory. Experimental results demonstrate the e ciencies of our approaches when compared with the related work. |
URI: | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/55095 |
DOI: | 10.6342/NTU202002154 |
Fulltext Rights: | 有償授權 |
Appears in Collections: | 資訊工程學系 |
Files in This Item:
File | Size | Format | |
---|---|---|---|
U0001-3107202013540600.pdf Restricted Access | 1.75 MB | Adobe PDF |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.