基於設計期契約與運行期調適之系統最佳化

Abstract

大型網宇實體系統的設計因其異質性、多供應商分散式開發，以及對安全性與效能的嚴苛要求而變得複雜。契約式設計透過為元件指定對環境的假設以及行為的保證，來管理此複雜性。儘管基於「假設－保證」之契約式設計能在開發階段促進模組化設計與可擴展的系統整合，但若運行階段假設被違反，便無法提供保證。契約式設計之效益因現代網宇實體系統運行於動態且不確定的環境中而受限。本論文在契約式設計的基礎上，探討運行期監控與違規處理，以強化系統的可靠性。 本論文提出了適用於完全去中心化任務卸載的契約形式，並以車載邊緣運算為案例進行驗證。我們透過實驗結果展示，由契約引導的啟發式分散式方法能在大幅降低設計成本的同時，達到優於進階方法之效能。雖然此種契約式設計能在部署前提供嚴謹的推理，但仍會因運行階段假設違反而無法提供保證。為此，本論文基於現有的運行期監控和違規處理技術，開發適用於動態場景的機制，以應對契約式設計所面臨的挑戰。首先，本論文針對參數化監控在記憶體資源受限時之可擴展性問題進行改進，為基於二元決策圖的參數化監控設計只允許單向誤判之近似演算法，在動態調整記憶體用量的同時保證監控正確性。其次，本論文開發了基於布隆過濾器的運行期監控器生成工具，提供通用且可調適的輕量監控解決方案。最後，本論文將重點由違規偵測延伸至違規調適。在車載控制任務卸載延遲回應的情境中，本論文提出基於多項式的輕量預測與平滑方法，使車輛能在通訊延遲下仍維持穩定的自動駕駛效能。 透過提出形式化契約與運行期調適機制，本論文不僅發揮了契約式設計於設計階段的模組化設計與可擴展整合優勢，更進一步提升了網宇實體系統在動態與不確定環境中的系統表現。

The design of large-scale cyber-physical systems (CPS) is complicated by their heterogeneity, distributed development across multiple vendors, and stringent requirements on both safety and performance. Contract-based design has emerged as a promising methodology to manage this complexity by specifying each component with assumptions on its environment and guarantees on its behavior. While assume-guarantee contracts enable modular design and scalable system integration at design time, they provide no guarantees once assumptions are violated at runtime. As modern CPS operate in dynamic and uncertain environments, the effectiveness of contract-based design alone becomes limited. This dissertation builds on contract-based design and investigates runtime monitoring and violation handling to strengthen system dependability. We present a contract formulation for fully decentralized task offloading. Using vehicular edge computing as a case study, we show that heuristic decentralized methods guided by contracts can achieve a task completion rate higher than the advanced approach while significantly reducing design cost. Although such contract-based design can provide rigorous reasoning before deployment, it fails to offer guarantees once assumptions are violated at runtime. To address this challenge, we extend existing runtime monitoring and violation handling techniques to develop mechanisms suitable for dynamic scenarios, thereby tackling the challenges faced by contract-based CPS. First, we investigate an existing parametric monitoring framework that employs binary decision diagrams (BDDs) and improve its scalability by introducing one-sided approximation algorithms that preserve soundness while adapting to dynamic memory constraints. Second, we develop a generic monitor generator that compiles annotated specifications into monitoring artifacts based on Bloom filters, xor filters, or binary fuse filters, providing lightweight and tunable monitoring solutions. Finally, we move beyond detection to violation adaptation. In the context of delayed responses in offloaded vehicular control, we propose polynomial-based prediction and smoothing methods that allow vehicles to maintain stable control performance despite communication delays. By introducing formal contracts and adaptive runtime mechanisms, this dissertation not only leverages the modular reasoning and scalable integration advantages of contract-based design at design time but also enhances the robustness and performance of CPS in dynamic and uncertain environments.