[發明專利]一種安全協議建模端與驗證端的跨平臺方法、計算機及存儲介質

在審

• 申請號: 202011376723.3
• 申請日: 2020-11-30
• 公開（公告）號: CN112506489A
• 公開（公告）日: 2021-03-16
• 發明（設計）人: 何錦龍;劉知昊;王沁煜;李勇堅;吳志林
• 申請（專利權）人: 廣州市智能軟件產業研究院
• 主分類號: G06F8/30
• 分類號: G06F8/30;G06F8/41
• 代理公司: 廣州微斗專利代理有限公司 44390
• 代理人: 陳文爽

本發明涉及一種安全協議建模端與驗證端的跨平臺方法，包括如下步驟：獲取建模模型的數據；使用XML文件來描述建模模型的數據；使用抽象語法樹作為多平臺驗證器和/或代碼生產器的中間表示；建模模型的數據模型傳輸至所述抽象語法樹，并通過腳本文件建立從模型工具到多平臺驗證器和/或代碼生成器的控制流；該安全協議建模端與驗證端的跨平臺方法、計算機及介質普適性強，且能夠保證模型數據流和對驗證器和/或編碼器的控制流的有效傳遞不受影響。

技術領域

本發明涉及計算機技術領域，特別涉及一種安全協議建模端與驗證端的跨平臺方法、計算機及存儲介質。

背景技術

針對形式化建模和驗證套件研制難度大、建模模型和驗證器模型之間集成困難、不同驗證器模型之間異構程度大等問題，可以從建模和形式化驗證模型中抽象出一套通用的表示方法。從具體實現的角度來看，形式化建模和驗證套件需要為用戶使用圖形建模語言建立的前端模型和后端集成的形式化驗證器、代碼自動生成器等設計一套關聯性強、語義明確、易于轉換的導出方案。

目前的主流的形式化建模和驗證套件雖然能夠在自己的建模前端和驗證器后端之間較好的做到這一點，但其表示格式往往是一種領域特定語言(Domain SpecificLanguage)，一方面需要自己的解析方式，另一方面不具有通用性，當用戶需要使用既有的建模端配合其它驗證器作為后端時，就需要自己實現兩類DSL的端到端翻譯器(Source ToSource Translator)，不僅難以保證兩類DSL具備語義包含關系，在實現翻譯器上也較為困難。

因此產生了對普適的從建模前端到驗證器后端的跨平臺表示格式的需求，需要能夠用統一的方式對驗證器后端進行集成，同時保證模型的數據流和對驗證器的控制流的有效傳遞不受影響。

發明內容

基于此，有必要提供一種普適的從建模模型到驗證器的跨平臺的方法。

本發明提供一種安全協議建模端與驗證端的跨平臺方法，包括如下步驟：

獲取建模模型的數據；

使用XML文件來描述建模模型的數據；

使用抽象語法樹作為多平臺驗證器和/或代碼生產器的中間表示；

建模模型的數據模型傳輸至所述抽象語法樹，并通過腳本文件建立從模型工具到多平臺驗證器和/或代碼生成器的控制流。

優選地，所述使用XML文件來描述建模模型的數據包括：

確定基于可擴展標記語言從建模模型向驗證器的模型表示范式，使用XML元數據和XML屬性來標識模型中的數據類型、進程模板、運行狀態、公理、初始知識、信道模板、狀態結點和遷移的內容；

確定基于可擴展標記語言從建模模型向驗證器的模型解析流程，對模型自底向上多次掃描以獲取數據類型、進程模板、運行狀態、初始知識、信道模板、狀態結點和遷移的內容，并保持其間的引用關系。

優選地，所述掃描包括第一次掃描，第一次掃描時，獲取協議中的數據類型、進行模板、運行狀態及狀態之間的轉移邊和連線關系。

優選地，所述數據類型包括自定義復合數據類型，所述掃描包括第二次掃描，第二次掃描時，確認協議中的自定義復合數據類型的屬性和通信方法，確認協議中進程模板的的屬性和通信方法。

優選地，對于用戶自定義的復合數據類型，還可以在標簽元素的內部添加屬性標簽，同時記錄屬性的類型、標識符和是否是數組屬性；所述標簽屬性為：Attribute type＝identifier＝isArray＝/。

優選地，所述掃描包括第三次掃描，第三次掃描時，確定協議中的初始知識、該初始知識引用的進程模板、單知識和公鑰私鑰對；還確認協議中的功能安全性質和信息安全性質。