以雙重弱硬式限制驗證系統性質

Abstract

嵌入式和網宇實體系統的不斷發展引領了實時系統管理的新模式，其中，嚴格的傳統實時限制通常無法容忍錯誤，因此常常與動態且不可預測的環境發生衝突。弱硬式錯誤模型（weakly-hard fault model）作為一種實用的解決方案，允許系統在控制下容忍特定次數的錯誤，進而實現了可靠性和適應性的平衡。準確地說，一個弱硬式錯誤模型使用單一重弱硬式限制 C = (m,k)（weakly-hard constraint）來描述，代表在 k 個連續的事件中，可以確保最多只有 m 個錯誤的事件。本論文提出了一種以雙重弱硬式限制驗證系統性質的創新方法，我們使用一個弱硬式限制對(C1,C2)來約束系統的輸入，並且提出不同的方法以高效地在所有可能的限制對下驗證系統性質。透過離散二階控制和網絡路由的兩個案例研究，這些方法的普遍性和有效性得到證實。實驗結果進一步表明，這種採用弱硬式限制對的模型能夠涵蓋更廣泛的系統行為範圍，突顯了其增強嵌入式和網宇實體系統靈活性和適應性的潛力，這對於此類需要在有限資源和存在錯誤的情況下提供保證的系統尤為重要。

The evolving landscape of embedded and cyber-physical systems has ushered in a new paradigm in real-time systems management, where the rigidity of traditional hard real-time constraints often conflicts with the need for flexibility in dynamic and unpredictable environments. The weakly-hard constraint model, defined by a weakly-hard constraint C = (m, k), where 0 ≤ m ≤ k, meaning that there are at most m bad events (faults) among any k consecutive events. It emerges as a pragmatic solution allowing a controlled number of faults, balancing reliability and adaptability. This thesis introduces an innovative methodology for verifying system properties under dual weakly-hard constraints. We have developed general approaches to verify properties for all possible values of weakly-hard constraint pairs (C_1,C_2), where C_i is a weakly-hard constraint with k_i being smaller than or equal to a given K. The process of verifying these candidates is executed precisely and efficiently, informed by our observation and analysis. We also introduce the speedup in m and k approaches, demonstrating their efficiency in managing larger state spaces for the special case of reachability analysis. If the system environment satisfies the weakly-hard requirements, the satisfaction of desired properties is assured. This assurance is particularly crucial for systems that must provide guarantees with limited resources and in the presence of faults. Through two case studies – discrete second-order control and network routing – we validate the effectiveness of our approaches. Our results indicate a substantial improvement in verification efficiency with the dual weakly-hard constraint model. The ability of this model to encompass a broader range of system behaviors underscores its potential to enhance the flexibility and adaptability of embedded and cyber-physical systems.