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

有效

• 申請?zhí)枺?/td>: 201310723208.1
• 申請日: 2013-12-25
• 公開（公告）號: CN103699743B
• 公開（公告）日: 2017-01-25
• 發(fā)明（設(shè)計）人: 周興社;拓明福;張凡;楊剛;單黎君;楊亞磊;張軍
• 申請（專利權(quán)）人: 西北工業(yè)大學(xué)
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 暫無信息
• 代理人: 暫無信息

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

步驟1：對混成系統(tǒng)描述語言HYSDEL進行擴展，得到在CPS-ADL平臺中對CPS行為建模的語言E-HYSDEL；

在HYSDEL聲明部分INTERFACE中添加時間的聲明，這部分時間屬性的聲明包括兩部分：連續(xù)狀態(tài)變化的連續(xù)時間變量t_x以及輸入控制量的時間t_u或T_s，其中連續(xù)狀態(tài)變化的時間t_x表示當(dāng)前系統(tǒng)物理實體的時間，t_u表示連續(xù)的輸入控制量u的時間，T_u則表示離散的輸入控制量U的時間戳；

步驟2：給出混合程序模型HPM的形式化定義：

HPM=（PD，VD，PC，SHPS）

其中，PD表示參數(shù)聲明；VD表示動態(tài)變量聲明；PC表示前置條件，也就是系統(tǒng)運行前各數(shù)據(jù)滿足的條件；SHPS表示混合程序中包含的子混合程序模型SHP集合，每個SHP的形式化定義如下：

SHP=（MS，DTS，CTS）

MS（Mode?Set）表示離散狀態(tài)模式的集合；DTS表示離散狀態(tài)遷移集合，即Mode之間的遷移；CTS表示連續(xù)遷移集合，描述單個Mode內(nèi)部的連續(xù)變化過程；

步驟3：建立CPS-ADL模型元素與HPM元素之間的轉(zhuǎn)換規(guī)則：

CPS-ADL各個模型元素由E-HYSDEL的不同函數(shù)進行描述，建立兩種模型之間的元素轉(zhuǎn)換規(guī)則主要是給出CPS-ADL模型中的函數(shù)與HPM中各元素之間的映射關(guān)系，按照內(nèi)容不同，把轉(zhuǎn)換規(guī)則分為數(shù)據(jù)轉(zhuǎn)換規(guī)則、結(jié)構(gòu)轉(zhuǎn)換規(guī)則、模式轉(zhuǎn)換規(guī)則、遷移轉(zhuǎn)換規(guī)則和約束轉(zhuǎn)換規(guī)則五類；

步驟4：在CPS-ADL平臺上采用擴展的混成自動機描述語言E-HYSDEL對CPS進行建模；

步驟5：利用步驟3中建立的兩種模型元素間的轉(zhuǎn)換規(guī)則，根據(jù)步驟4中建立的CPS模型生成HPM，然后根據(jù)HPM得到混合程序；

步驟6：將需要驗證的CPS屬性描述為符合微分動態(tài)邏輯的屬性約束公式，進行必要的規(guī)約；

步驟7：根據(jù)定理證明器KeYmaera的輸入格式要求，將步驟5中得到的混合程序和步驟6中得到的待驗證屬性公式格式化，最后生成KeYmaera的輸入代碼；

對照HP表示法和KeYmaera輸入表示法，替換HP中運算符、標識符等語法元素，添加必要的輔助標識，調(diào)整構(gòu)成元素的位置和結(jié)構(gòu)；

步驟8：在定理證明器KeYmaera中打開步驟7中得到的輸入代碼文件，進行驗證，得到驗證結(jié)論。

2.根據(jù)權(quán)利要求1所述的基于CPS-ADL模型向混合程序轉(zhuǎn)換的CPS建模與驗證方法，其特征在于，步驟3中所述數(shù)據(jù)轉(zhuǎn)換規(guī)則、結(jié)構(gòu)轉(zhuǎn)換規(guī)則、模式轉(zhuǎn)換規(guī)則、遷移轉(zhuǎn)換規(guī)則和約束轉(zhuǎn)換規(guī)則具體為：

數(shù)據(jù)轉(zhuǎn)換規(guī)則：將INTERFACE部分的INPUT函數(shù)、INTERFACEOUTPUT函數(shù)和AUX函數(shù)映射為HPM中的元素VD；將PARAMETER函數(shù)映射為HPM中的元素PD；

結(jié)構(gòu)轉(zhuǎn)換規(guī)則：將STATE函數(shù)中的每個狀態(tài)變量轉(zhuǎn)換為一個SHP，從而STATE函數(shù)映射為SHPS；

模式轉(zhuǎn)換規(guī)則：從AD函數(shù)、DA函數(shù)、LOGIC函數(shù)、COUTINUOUS函數(shù)、LINEAR函數(shù)和AUTOMATA函數(shù)映射各SHP中的MS，布爾型變量對應(yīng)兩個Mode，連續(xù)型變量對應(yīng)的Mode數(shù)量與其函數(shù)式的分段數(shù)量相等，每個Mode的基本屬性包括名稱、類型等，對于連續(xù)型變量對應(yīng)的Mode，還要描述變量在當(dāng)前Mode下的變化公式，進一步，根據(jù)變量間的依賴關(guān)系將Mode加入到相應(yīng)HPM的MS中，同一個Mode若與多個狀態(tài)變量有直接或間接依賴關(guān)系，則可加入到多個HPM的MS中，若兩個Mode分別是某個遷移的源節(jié)點和目標節(jié)點，則加入到相同的HPM中；

遷移轉(zhuǎn)換規(guī)則：從AD函數(shù)、DA函數(shù)、LOGIC函數(shù)、COUTINUOUS函數(shù)、LINEAR函數(shù)和AUTOMATA函數(shù)映射各SHP中的DTS和CTS，分支結(jié)構(gòu)的一個分支對應(yīng)一個遷移，遷移規(guī)則描述包括源節(jié)點、目標節(jié)點、遷移觸發(fā)條件和遷移輸出，根據(jù)遷移的源節(jié)點和目標節(jié)點，將遷移加入相應(yīng)的SHP；

約束轉(zhuǎn)換規(guī)則：將MUST函數(shù)以及INPUT函數(shù)和STATE中對變量取值的限定條件轉(zhuǎn)換為HPM中的PC。