請用此 Handle URI 來引用此文件:
http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/55095
完整後設資料紀錄
DC 欄位 | 值 | 語言 |
---|---|---|
dc.contributor.advisor | 林忠緯(Chung-Wei Lin) | |
dc.contributor.author | Kai-Chieh Chang | en |
dc.contributor.author | 張凱捷 | zh_TW |
dc.date.accessioned | 2021-06-16T03:47:03Z | - |
dc.date.available | 2020-08-07 | |
dc.date.copyright | 2020-08-07 | |
dc.date.issued | 2020 | |
dc.date.submitted | 2020-07-31 | |
dc.identifier.citation | [1] L. Ahrendts, S. Quinton, T. Boroske, and R. Ernst, 'Verifying Weakly-Hard Real-Time Properties of Traffic Streams in Switched Networks,' in 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), ser. Leibniz International Proceedings in Informatics (LIPIcs), S. Altmeyer, Ed., vol. 106, pp. 15:1-15:22. Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018. [Online]. Available: http://drops.dagstuhl.de/opus/volltexte/2018/8987 [2] G. Bernat, A. Burns, and A. Liamosi, 'Weakly hard real-time systems,' IEEE Transactions on Computers, vol. 50, no. 4, pp. 308-321, Apr 2001. [3] G. Bernat and R. Cayssials, 'Guaranteed on-line weakly-hard real-time systems,' in The IEEE Real-Time Systems Symposium, pp. 22-35, 2001. [4] R. Blind and F. Allgower, 'Towards networked control systems with guaranteed stability: Using weakly hard real-time constraints to model the loss process,' in IEEE Conference on Decision and Control, pp. 7510-7515. IEEE, 2015. [5] X. Chen, E. Abrah am, and S. Sankaranarayanan, 'Flow*: An analyzer for non-linear hybrid systems,' in International Conference on Computer-Aided Verification, pp. 258-263. Springer, 2013. [6] H. Choi, H. Kim, and Q. Zhu, 'Job-class-level fixed-priority scheduling of weakly-hard real-time systems,' in IEEE Real-Time Technology and Applications Symposium (RTAS), 2019. [7] P. S. Duggirala and M. Viswanathan, 'Analyzing real-time linear control systems using software verification,' in IEEE Real-Time Systems Symposium, pp. 216-226. IEEE, 2015. [8] FBK-irst, Carnegie Mellon University, University of Genova, and University of Trento. (2015) NuSMV v2.6.0. [Online; Accessed on Oct. 23, 2019]. [Online]. Available: http://nusmv.fbk.eu/ [9] G. Frehse, A. Hamann, S. Quinton, and M. Woehrle, 'Formal analysis of timing effects on closed-loop properties of control software,' in IEEE Real-Time Systems Symposium, pp. 53-62, 2014. [10] G. Frehse, C. Le Guernic, A. Donz e, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler, 'Spaceex: Scalable verification of hybrid systems,' in International Conference on Computer-Aided Veri cation, pp. 379-395. Springer, 2011. [11] A. Gujarati, M. Nasri, R. Majumdar, and B. B. Brandenburg, 'From iteration to system failure: Characterizing the fitness of periodic weakly-hard systems,' in Euromicro Conference on Real-Time Systems, pp. 9:1-9:23, 2019. [12] M. Hamdaoui and P. Ramanathan, 'A dynamic priority assignment technique for streams with (m, k)- rm deadlines,' IEEE Transactions on Computers, vol. 44, no. 12, pp. 1443-1451, 1995. [13] Z. A. H. Hammadeh, R. Ernst, S. Quinton, R. Henia, and L. Rioux, 'Bounding deadline misses in weakly-hard real-time systems with task dependencies,' inDesign, Automation Test in Europe Conference Exhibition (DATE), 2017, pp. 584-589, March 2017. [14] Z. A. H. Hammadeh, S. Quinton, M. Panunzio, R. Henia, L. Rioux, and R. Ernst, 'Budgeting Under-Specified Tasks for Weakly-Hard Real-Time Systems,' in 29th Euromicro Conference on Real-Time Systems (ECRTS 2017), ser. Leibniz International Proceedings in Informatics (LIPIcs), M. Bertogna, Ed., vol. 76, pp. 17:1-17:22. Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. [Online]. Available: http://drops.dagstuhl.de/opus/volltexte/2017/7163 [15] C. Huang, K. Wardega, W. Li, and Q. Zhu, 'Exploring weakly-hard paradigm for networked systems,' in Workshop on Design Automation for CPS and IoT (DESTION'19), 2019. [16] C. Huang, W. Li, and Q. Zhu, 'Formal verification of weakly-hard systems,' in ACM International Conference on Hybrid Systems: Computation and Control, pp. 197-207. [17] V. Lesi, I. Jovanov, and M. Pajic, 'Network scheduling for secure cyber-physical systems,' in IEEE Real-Time Systems Symposium (RTSS), pp. 45-55, Dec 2017. [18] J. Li, Y. Song, and F. Simonot-Lion, 'Providing real-time applications with graceful degradation of QoS and fault tolerance according to (m; k)-firm model,' IEEE Transactions on Industrial Informatics, vol. 2, no. 2, pp. 112-119, 2006. [19] S. Linsenmayer and F. Allgower, 'Stabilization of networked control systems with weakly hard real-time dropout description,' in IEEE Conference on Decision and Control, pp. 4765-4770, 2017. [20] P. Pazzaglia, C. Mandrioli, M. Maggio, and A. Cervin, 'DMAC: Deadline-miss aware control,' in Euromicro Conference on Real-Time Systems, pp. 1:1-1:24, 2019. [21] S. Prajna, P. A. Parrilo, and A. Rantzer, 'Nonlinear control synthesis by convex optimization,' IEEE Transactions on Automatic Control, vol. 49, no. 2, pp. 310-314, 2004. [22] S. Quinton and R. Ernst, 'Generalized weakly-hard constraints,' in International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, pp. 96-110. Springer, 2012. [23] L. Schenato, 'To zero or to hold control inputs with lossy links?' IEEE Transactions on Automatic Control, vol. 54, no. 5, pp. 1093-1099, 2009. [24] Y. Sun and M. D. Natale, 'Weakly hard schedulability analysis for fixed-priority scheduling of periodic real-time tasks,' ACM Transactions on Embedded Computing Systems, vol. 16, no. 5s, pp. 171:1-171:19, 2017. [25] L. Thiele, S. Chakraborty, and M. Naedele, 'Real-time calculus for scheduling hard real-time systems,' in IEEE International Symposium on Circuits and Systems (ISCAS), vol. 4, pp. 101-104 vol.4, May 2000. [26] Uppsala University and Aalborg University. (2014) UPPAAL v4.0.14. [Online; Accessed on Oct. 23, 2019]. [Online]. Available: http://www.uppaal.org/ [27] W. Xu, Z. A. H. Hammadeh, A. Kroller, R. Ernst, and S. Quinton, 'Improved deadline miss models for real-time systems using typical worst-case analysis,' in Euromicro Conference on Real-Time Systems, pp. 247-256, 2015. | |
dc.identifier.uri | http://tdr.lib.ntu.edu.tw/jspui/handle/123456789/55095 | - |
dc.description.abstract | 隨著當今系統架構設計複雜度的提升,硬式即時系統要求顯得過於嚴格,於是弱硬式系統的概念便被提出來緩和限制,允許特定數量的死線被錯過。一個弱硬式限制可以由 (m, k) 來描述,表示在連續的k 個事件中,最多只允許有m 個事件錯過對應的死線。這篇論文考慮了兩種不同的系統模型,分別是離散的有限狀態機和連續的動態系統,我們首先提出了建構安全狀態表的方法,其中包含了所有可能的 (m, k),接著展示狀態壓縮的技巧來解決特定的 (m, k),再進一步的使用了分層廣度優先遍歷來有效率的 建構出這張表。此外我們也研究出了方格剖分技巧,將連續的難題轉化為一個離散的圖論問題,安全起始區域便可通過連通性分析來獲得。在實驗結果的部分,我們展現出新算法的效率與正確性,以及對比於一些相關研究的優點。 | zh_TW |
dc.description.abstract | 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. | en |
dc.description.provenance | Made available in DSpace on 2021-06-16T03:47:03Z (GMT). No. of bitstreams: 1 U0001-3107202013540600.pdf: 1787594 bytes, checksum: c8d8dd35124777e2d6a598fe7cda6a39 (MD5) Previous issue date: 2020 | en |
dc.description.tableofcontents | Acknowledgments ii Abstract (Chinese) iii Abstract iv List of Tables vii List of Figures viii Chapter 1. Introduction 1 1.1 Introduction to Weakly-Hard Model . . . . . . . . . . . . . . . . . . . . 1 1.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Our Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.4 Thesis Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Chapter 2. De nition 6 2.1 System Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.1 Non-Deterministic Finite-State Machine . . . . . . . . . . . . . . 6 2.1.2 Continuous Dynamical System . . . . . . . . . . . . . . . . . . . . 7 2.2 Fault Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.1 Weakly-Hard Model . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.2.2 Common Fault Models . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3 Problem De nition . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Chapter 3. Our Algorithm 10 3.1 Algorithms Overview . . . . . . . . . . . . . . . . . . . . . . . . 10 3.2 Non-Deterministic Finite-State Machines . . . . . . . . . . . . . . 11 3.2.1 Reachability Analysis for Fixed (m; k) . . . . . . . . . . . . . . 11 3.2.2 Approach 1: Machines Composition . . . . . . . . . . . . . . . . . 12 3.2.3 Approach 2: Mask Compression . . . . . . . . . . . . . . . . . . . 14 3.2.4 Reachability Analysis for All (m; k) . . . . . . . . . . . . . . . 16 3.2.5 Approach 1: Brute Force . . . . . . . . . . . . . . . . . . . . . 18 3.2.6 Approach 2: Monotonic Properties . . . . . . . . . . . . . . . . . 18 3.2.7 Approach 3: Layered Breadth-First Search (BFS) . . . . . . . . . . 21 3.2.8 Reachability Approximation for Larger K . . . . . . . . . . . . . 24 3.3 Continuous Dynamical Systems . . . . . . . . . . . . . . . . . . . . 26 3.3.1 SAW Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 3.3.2 Construct Reachability Graph . . . . . . . . . . . . . . . . . . . 28 3.3.3 DP-based Local Safety Set Search . . . . . . . . . . . . . . . . . 30 3.3.4 Reverse Inductiveness Set Search . . . . . . . . . . . . . . . . . 32 Chapter 4. Experimental Results 33 4.1 Non-Deterministic Finite-State Machine . . . . . . . . . . . . . . . 33 4.1.1 Periodic Fault Model . . . . . . . . . . . . . . . . . . . . . . . 34 4.1.2 Weakly-Hard Fault Model . . . . . . . . . . . . . . . . . . . . . 35 4.2 Continuous Dynamical Systems . . . . . . . . . . . . . . . . . . . . 37 4.2.1 Comparison with One-Dimension Abstraction . . . . . . . . . . . . 38 4.2.2 Impact of (m;K), Granularity, and Stepsize . . . . . . . . . . . . 38 4.2.3 Example Usage . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Chapter 5. Conclusions 43 Bibliography 44 | |
dc.language.iso | en | |
dc.title | 弱硬式系統之正規驗證 | zh_TW |
dc.title | Formal Verification of Weakly-Hard Systems | en |
dc.type | Thesis | |
dc.date.schoolyear | 108-2 | |
dc.description.degree | 碩士 | |
dc.contributor.oralexamcommittee | 陳偉松(Tony Tan),蕭旭君(Hsu-Chun Hsiao),江介宏(Jie-Hong Jiang) | |
dc.subject.keyword | 弱硬式系統,系統安全驗證,圖論, | zh_TW |
dc.subject.keyword | Weakly-Hard systems,Safety veri cation,Graph theory, | en |
dc.relation.page | 48 | |
dc.identifier.doi | 10.6342/NTU202002154 | |
dc.rights.note | 有償授權 | |
dc.date.accepted | 2020-08-03 | |
dc.contributor.author-college | 電機資訊學院 | zh_TW |
dc.contributor.author-dept | 資訊工程學研究所 | zh_TW |
顯示於系所單位: | 資訊工程學系 |
文件中的檔案:
檔案 | 大小 | 格式 | |
---|---|---|---|
U0001-3107202013540600.pdf 目前未授權公開取用 | 1.75 MB | Adobe PDF |
系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。