[發明專利]計及信息時效的嵌入式裝置安全通信協議驗證方法和系統

在審

• 申請號: 202010021115.4
• 申請日: 2020-01-09
• 公開（公告）號: CN111211945A
• 公開（公告）日: 2020-05-29
• 發明（設計）人: 梁云;黃莉;倪傳坤;汪強;陳獻慶;童和欽;張喬賓
• 申請（專利權）人: 全球能源互聯網研究院有限公司;許繼集團有限公司;國網遼寧省電力有限公司;國網遼寧省電力有限公司電力科學研究院;南瑞集團有限公司;國家電網有限公司
• 主分類號: H04L12/26
• 分類號: H04L12/26;H04L12/24
• 代理公司: 北京安博達知識產權代理有限公司 11271
• 代理人: 徐國文

1.計及信息時效的嵌入式裝置安全通信協議驗證方法，其特征在于，所述方法包括以下步驟：

對預先建立的狀態與變遷模型中各層級進行狀態空間搜索，驗證安全通信過程的時效性是否正確；

基于所述嵌入式裝置安全通信過程的時效性，對所述狀態與變遷模型中的通信時間消耗進行分析，驗證安全通信過程是否可以在預定的時間內完成；

其中，所述狀態與變遷模型，是通過將嵌入式裝置安全通信協議劃分后得到的多個層級構建的。

2.根據權利要求1所述的方法，其特征在于，所述狀態與變遷模型的建立，包括：

將嵌入式裝置安全通信協議分為應用系統、傳輸層、信道，以及消息交互過程；

基于所述應用系統、傳輸層、信道，以及消息交互過程構建應用系統模型層級、傳輸層模型層級和信道模型層級；

基于所述應用系統模型層級、傳輸層模型層級和信道模型層級結合著色petri網建模方法，構建狀態與變遷模型。

3.根據權利要求1所述的方法，其特征在于，所述狀態與變遷模型如下式：

M＝(L,Π,P,T,C,G,E)

其中，L表示嵌入式裝置安全通信協議的應用系統、傳輸層、信道三個模型層級，形成分層著色petri網模型；Π是模型中的顏色集，表示狀態類型與消息類型的集合；P表示著色petri網模型中的庫所集合，包括存儲狀態的庫所，以及存儲輸入輸出消息的庫所；T表示變遷集合，包括模型層級L間的變遷，以及傳輸消息和狀態轉換的變遷；C表示P和Π的對應關系；G表示包括消息傳輸和狀態轉換的條件函數；E表示傳輸消息或轉換狀態的表達式函數。

4.根據權利要求1所述的方法，其特征在于，所述對所述狀態與變遷模型中各層級進行狀態空間搜索，驗證安全通信過程的時效性是否正確；包括：

基于庫所集合、變遷集合得到嵌入式裝置安全通信協議對應的petri網結構；

基于嵌入式裝置安全通信協議執行的時效性，在信道模型中定義時間約束和隨機因素；

基于petri網模型的關聯矩陣，驗證所述狀態與變遷模型的有界性；

使用形式化驗證工具進行狀態空間搜索，同時使用內嵌分支時序邏輯，用命題的形式表示嵌入式裝置安全通信協議能夠進入安全連接狀態；

當命題成立時，安全通信過程的時效性正確，否則，安全通信過程的時效性不正確。

5.如權利要求4所述的方法，其特征在于，所述安全通信協議的時序不正確時，進行反例的查找。

6.根據權利要求1所述的方法，其特征在于，所述基于所述嵌入式裝置安全通信協議執行的時效性，對所述狀態與變遷模型中的通信時間消耗進行分析，驗證安全通信過程是否可以在預定的時間內完成包括：

基于嵌入式裝置安全通信協議執行的時效性為各模型層級中設置的時間約束和隨機因素；

基于所述時間約束和隨機因素對通信時間消耗進行分析，驗證安全通信過程是否可以在預定的時間內完成。

7.計及信息時效的嵌入式裝置安全通信協議驗證系統，其特征在于，所述系統包括：搜索模塊和分析模塊；

所述搜索模塊，用于對預先建立的狀態與變遷模型中各層級進行狀態空間搜索，驗證安全通信過程的時效性是否正確；

所述分析模塊，用于基于所述嵌入式裝置安全通信過程的時效性，對所述狀態與變遷模型中的通信時間消耗進行分析，驗證安全通信過程是否可以在預定的時間內完成；

其中，所述狀態與變遷模型，是通過將嵌入式裝置安全通信協議劃分后得到的多個層級構建的。

8.根據權利要求7所述系統，其特征在于，還包括：劃分模塊，所述劃分模塊，包括：交互單元、構建單元和結合單元；

所述交互單元，用于將嵌入式裝置安全通信協議分為應用系統、傳輸層、信道，以及消息交互過程；

所述構建單元，用于基于所述應用系統、傳輸層、信道，以及消息交互過程構建應用系統模型層級、傳輸層模型層級和信道模型層級；

所述結合單元，用于基于所述應用系統模型層級、傳輸層模型層級和信道模型層級結合著色petri網建模方法，構建狀態與變遷模型。