《嵌入式系統構件模型的領域語義檢查方法研究》是依託清華大學，由張荷花擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：嵌入式系統構件模型的領域語義檢查方法研究
- 依託單位：清華大學
- 項目負責人：張荷花
- 項目類別：青年科學基金項目
項目摘要,結題摘要,
項目摘要
構件化建模技術被廣泛套用於嵌入式系統的設計和開發。為確保嵌入式系統構件化建模的正確性，檢查構件之間連線是否正確至關重要。隨著構件模型的不斷增大，構件之間的連線互動增多，正確性檢查越來越困難。常規的語義檢查基於類型系統實現，能夠判定數據類型是否匹配，卻難以檢測更為豐富的領域語義約束，不能滿足嵌入式系統構件模型對正確性的嚴格要求。本項目研究能夠一致解決構件模型連線許可、單位、含義、錯位等多種錯誤的領域語義檢查方法。提出基於本體的領域約束描述語言，一致嚴格的描述各種領域約束；提出領域語義自動標註方法，建立構件與領域語義的有效映射；提出基於領域語義的構件模型一致性檢查方法，能夠自適應領域約束的變動。研究成果將針對如列車控制等套用領域，在多種嵌入式系統建模語言工具中進行實例驗證，以檢驗本研究方法的通用性和有效性。
結題摘要
本項目圍繞面向領域特定語義的嵌入式系統構件模型語義檢查方法開展研究，以便在靜態檢查階段，統一檢查與領域語義相關的連線許可、單位錯誤、含義混淆、連線錯位等問題，保證構件模型的正確性。在領域約束描述語言方面，針對靜態規則描述，提出了結構化自然語言語言SNL，具有表達能力強、易用、形式化等特徵，並研究了基於SNL的規則庫一致性和完備性檢查算法。在面向構件模型的領域語義標註和推理方面，建立了一套基於概念格的領域語義類型系統，基於約束求解器和描述邏輯推理進行語義類型兼容性檢查和領域規則檢查。在面向嵌入式系統的構件模型語義檢查方面，針對在基於可調度性規則的嵌入式系統體系結構分析、基於領域規則的嵌入式系統中斷程式建模和正確性檢查以及領域規則在同步異步融合建模和模型檢查方面開展了研究工作。實現了領域知識建模工具和構件模型通用語義檢查工具，並集成到Ptolemy II和Tsmart可信建模驗證工具集中，擴展了兩類工具的語義類型檢查、連線關係檢查、包含關係檢查等檢查能力。
