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

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

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

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

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

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

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