[發(fā)明專利]一種基于模型轉(zhuǎn)換的CPS建模與驗證方法

有效

• 申請?zhí)枺?/td>: 201110332336.4
• 申請日: 2011-10-28
• 公開（公告）號: CN102436375A
• 公開（公告）日: 2012-05-02
• 發(fā)明（設(shè)計）人: 李必信;朱敏;李加凱;陳喬喬;翟小祥
• 申請（專利權(quán)）人: 東南大學(xué)
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 南京天翼專利代理有限責(zé)任公司 32112
• 代理人: 朱戈勝

1.一種基于模型轉(zhuǎn)換的CPS建模與驗證方法，其特征包括如下步驟：

步驟1)分析給出微分動態(tài)邏輯方法驗證CPS的操作模型Hybrid?Programs的形式化描述：

用InitBlock表示初始化塊；

用DJ表示離散變遷的集合；

用CE表示連續(xù)變化的集合；

用HPSkeleton和HPContent分別表示Hybrid?Programs的框架和內(nèi)容；

步驟2)在HybridUML元模型數(shù)據(jù)結(jié)構(gòu)表示基礎(chǔ)上，增加：

Mode和Agent分類、頂層Mode、變遷的源和目標Mode、變遷分類的形式化表示；

步驟3)定義模型轉(zhuǎn)換規(guī)則的格式：

用RuleType表示規(guī)則的類型，規(guī)則的類型分為映射規(guī)則和處理規(guī)則；

用Mapping/Processing表示規(guī)則的映射或處理過程；

用Return?Result表示返回規(guī)則處理的結(jié)果；

步驟4)建立共享變量表規(guī)則CreateShare?VariableTable：

表的每一行表示Agent之間共享的變量，用于解決HybridUML中變量有作用域限定，而Hybrid?Programs中變量皆為全局變量的問題；

步驟5)進行HybridUML模型中靜態(tài)結(jié)構(gòu)到HPSkeleton的轉(zhuǎn)換；

步驟6)建立規(guī)則CreateTransitionPath，將一個變遷和以另一個變遷的目標Mode為源Mode的兩個變遷進行合并；

步驟7)建立規(guī)則EliminateJunction，將HybridUML的狀態(tài)圖中的分叉點進行合并；

步驟8)建立規(guī)則FlatHierarchyMode，根據(jù)變遷的種類將HybridUML狀態(tài)圖的層次進行展開；

步驟9)定義有向圖TransitionGraph表示展開后的簡單狀態(tài)圖，圖的頂點由HybridUML中原子Mode組成，頂點之間的邊表示以該兩個頂點為源和目標的變遷；

步驟10)建立變遷轉(zhuǎn)換的規(guī)則MappingTGtoHP，將TransitionGraph中的變遷轉(zhuǎn)換為Hybrid?Programs中的變遷；

步驟11)生成規(guī)則應(yīng)用的模板TemplateHUtoHP，組織步驟4)至步驟10)中建立的轉(zhuǎn)換規(guī)則，對輸入的HybridUML模型應(yīng)用模板生成相應(yīng)的Hybrid?Programs模型；

步驟12)利用微分動態(tài)邏輯公式對CPS屬性進行規(guī)約；

步驟13)根據(jù)定理證明器KeYmaera的輸入格式要求，將得到的Hybrid?Programs模型和步驟12)中的屬性公式進行格式化，最后生成KeYmaera的輸入代碼；

步驟14)將步驟13)得到的輸入代碼作為KeYmaera進行驗證。