[發明專利]通信協議可信性驗證裝置

有效

• 申請號: 202010011588.6
• 申請日: 2020-01-06
• 公開（公告）號: CN111245676B
• 公開（公告）日: 2022-03-04
• 發明（設計）人: 史建琦;黃滟鴻;張繼;任建鵬;于會新;楊洋;張鵬
• 申請（專利權）人: 上海豐蕾信息科技有限公司
• 主分類號: H04L43/18
• 分類號: H04L43/18;H04L69/00
• 代理公司: 北京辰權知識產權代理有限公司 11619
• 代理人: 付婧

1.一種通信協議可信性驗證裝置，其特征在于，包括：

形式化語言描述模塊，用于通過形式化語言描述滿足安全傳輸指標的需求規范，得到形式化語言描述的需求規范,所述安全傳輸指標的需求包括：系統接口需求、用戶界面需求、硬件接口需求、軟件接口需求、通信接口需求；

其中，所述形式化語言描述模塊，包括：分析單元，用于對所述滿足安全傳輸指標的需求規范進行詞法分析、語法分析、語義分析，得到分析結果；

形式化語言描述單元，用于通過形式化語言描述所述分析結果，選擇對應的語義抽象函數，建立形式化描述和等價類中的被描述對象的關系，通過使用不同的語義抽象函數，將被描述對象劃分成多個等價類，使每個等價類分別與不同形式化描述語言建立抽象關系，把多個形式化描述語言集成于同一個語義域，得到形式化語言描述的需求規范；

其中，在對協議進行建模時，為每一類節點賦予一個模型，并用進程代數描述語言對進程模型之間的通信進行描述，通過初始化異步幀消息的調度請求，以及對協議中的調度算法的建模，完成協議周期中調度幀信息的模擬，整個協議模型由不同類型節點的進程的并發組成；

形式化驗證模塊，用于通過形式化驗證工具對所述形式化語言描述的需求規范進行驗證，得到驗證數據集；

檢測模塊，用于根據所述驗證數據集，進行規范檢測。

2.根據權利要求1所述的裝置，其特征在于，所述形式化驗證工具，包括：

過程分析工具包(PAT)。

3.根據權利要求1所述的裝置，其特征在于，所述驗證數據集，包括：

正確性驗證數據集、完備性驗證數據集、一致性驗證數據集和無歧義性驗證數據集。

4.根據權利要求1所述的裝置，其特征在于，所述檢測模塊，包括：

正確性檢測單元，用于根據正確性驗證數據集，檢測規范是否正確；

完備性檢測單元，用于根據完備性驗證數據集，檢測規范是否完備；

一致性檢測單元，用于根據一致性驗證數據集，檢測規范是否一致；

無歧義性檢測單元，用于根據無歧義性驗證數據集，檢測規范是否無歧義。