隨著功能需求的不斷增加,安全關鍵系統(tǒng)的設計變得越來越復雜。如何通過建模與驗證的方法保證安全關鍵系統(tǒng)的質量,一直以來都是形式化方法領域備受關注的問題。AADL作為一種應用廣泛的建模語言,在安全關鍵系統(tǒng)的設計與實現中發(fā)揮著重要的作用。它提供了豐富的組件用來描述系統(tǒng)的體系結構,并且能夠支持性能關鍵屬性的早期預測和重復性分析。然而,AADL描述系統(tǒng)行為的方式主要是基于自動機理論,在建模和驗證大型復雜系統(tǒng)時難免會遇到狀態(tài)空間爆炸問題。此外,由于缺乏描述行為細節(jié)的手段,AADL難以支持功能需求的分析與驗證,從而無法保證整個系統(tǒng)的正確性和安全性。針對AADL語言在行為描述以及模型驗證上的不足,本文提出了一種基于約束求解的精化行為建模方法。該方法擴展了AADL語言以增強其描述行為細節(jié)的能力,并且能夠支持Z3求解器對構建的精化行為模型進行分析與驗證,從而在一定程度上緩解狀態(tài)空間爆炸的情形。本文的主要貢獻如下:(1)基于AADL語言的擴展機制,提出了一個能夠支持精化行為建模的附屬語言RBML,并給出它的語法和語義。該語言創(chuàng)新性地引入了自定義機制,用來提升行為建模時的靈活性。它允許用戶根據需要在RBML規(guī)范...

【文章頁數】：82 頁

【學位級別】：碩士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景和意義
    1.2 技術路線及研究內容
    1.3 國內外研究現狀
    1.4 論文組織
第二章 相關理論
    2.1 AADL語言
    2.2 Z3 求解器
    2.3 Modelica語言
    2.4 本章小結
第三章 精化行為建模語言RBML
    3.1 RBML語言的數據類型
    3.2 RBML語言的語法
    3.3 RBML語言的語義
    3.4 溫度控制系統(tǒng)的應用實例
    3.5 本章小結
第四章 RBML精化行為模型的驗證與仿真
    4.1 模型轉換的原理
    4.2 RBML到 SMT-LIB的轉換規(guī)則
    4.3 RBML到 Modelica的轉換規(guī)則
    4.4 RBML語言的模型轉換算法
    4.5 本章小結
第五章 AADL2ZAO工具的設計與實現
    5.1 RBML語言的元模型構建
    5.2 AADL2ZAO工具的框架設計
    5.3 AADL2ZAO工具的實現細節(jié)
    5.4 本章小結
第六章 案例研究與方法對比
    6.1 百度Apollo系統(tǒng)介紹
    6.2 Apollo系統(tǒng)的RBML建模
    6.3 離散行為的Z3 驗證
    6.4 連續(xù)行為的Modelica仿真
    6.5 方法對比與性能分析
    6.6 本章小結
第七章 總結與展望
    7.1 總結
    7.2 展望
參考文獻
致謝
研究成果



本文編號：3881136