弱硬式網宇實體系統之驗證與排程性分析

Abstract

一個弱硬式錯誤模型可以用(m, k)來描述，代表在k個連續的事件中，最多只有m個錯誤的事件。這篇論文我們用弱硬式錯誤模型來約束系統的一個輸入，我們提出的方法可以快速的在所有可能的(m, k)下驗證系統的性質，在驗證完所有的(m, k)後，我們可以知道系統需要被約束在甚麼條件下才能保有該性質，並且我們可以設計一個即時監控來偵測目前錯誤的數量，如果偵測到的系統輸入符合弱硬式條件的需求，我們可以保證系統的性質；否則，即時監控可以讓系統進入到一個安全的模式。這對於需要在有限資源和存在錯誤的情況下提供保證的網宇實體系統尤其重要，離散二階控制、網絡路由、車輛跟隨和車道變換的實驗結果證明了所提出方法的普遍性和效率。此外，考慮到多個系統共享一個處理器，需要一個排程器，由於在排程過程中應保證系統的特性，系統設計人員可以將驗證結果中的弱硬約束分配給系統。調度器必須確保資源分配能夠滿足約束，我們還提出了多個弱硬條件下的排程性分析方法，並將我們的方法與其他排程性分析方法進行比較以證明其通用性。驗證可以為系統設計提供策略，排程性分析可以幫助系統設計人員分析策略是否可行。

A weakly-hard fault model can be captured by an (m,k) constraint, where 0 <= m <= k, meaning that there are at most m bad events (faults) among any k consecutive events. In this thesis, we use a weakly-hard fault model to constrain the occurrences of faults in system inputs. We develop approaches to verify properties for all possible values of (m,k), where k is smaller than or equal to a given K, in an exact and efficient manner. By verifying all possible values of (m,k), we define weakly-hard requirements for the system environment and design a runtime monitor based on counting the number of faults in system inputs. If the system environment satisfies the weakly-hard requirements, the satisfaction of desired properties is guaranteed; otherwise, the runtime monitor can notify the system to switch to a safe mode. This is especially essential for cyber-physical systems which need to provide guarantees with limited resources and the existence of faults. Experimental results with discrete second-order control, network routing, vehicle following, and lane changing demonstrate the generality and the efficiency of the proposed approaches. Moreover, considering multiple systems sharing a processor, a scheduler is needed. Since properties of systems should be guaranteed during the scheduling process, system designers can assign weakly-hard constraints from the verification results to systems. The scheduler has to make sure the resources distribution can satisfy the constraints. We also propose the schedulability analysis method under multiple weakly-hard constraints and compare our method with other schedulability analysis methods to demonstrate the generality. The verification can give the strategy to system design ,and the schedulability analysis can help system designers analyze whether the strategy is feasible or not.