[發明專利]形式化任務驗證方法、裝置、電子設備和計算機可讀介質

有效

• 申請號: 202010215783.0
• 申請日: 2020-03-24
• 公開（公告）號: CN111427785B
• 公開（公告）日: 2023-08-18
• 發明（設計）人: 馮斯文
• 申請（專利權）人: 北京金山云網絡技術有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京超凡宏宇專利代理事務所(特殊普通合伙) 11463
• 代理人: 安衛靜

1.一種形式化任務驗證方法，其特征在于，包括：

獲取待驗證任務的任務流的配置文件，其中，所述任務流的配置文件中包含以下至少一種配置信息：任務流的變量信息，所述變量信息的初始參數，所述變量信息的狀態變更信息，所述任務流的驗證條件；

基于所述任務流的配置文件中所包含的配置信息構建目標驗證文件，其中，所述目標驗證文件為基于形式化驗證語言構建的文件；

基于所述目標驗證文件對所述任務流的時序狀態進行形式化驗證；

基于所述任務流的配置文件中所包含的配置信息構建目標驗證文件包括：

利用解析關鍵字對所述任務流的配置文件進行解析，得到所述至少一種配置信息；解析關鍵字為：變量、初始參數、任務、狀態變更和驗證條件；

利用所述形式化驗證語言對所述至少一種配置信息進行編譯，得到所述目標驗證文件。

2.根據權利要求1所述的方法，其特征在于，基于所述任務流的配置文件中所包含的配置信息構建目標驗證文件包括：

獲取預設映射關系，其中，所述預設映射關系為所述任務流的配置文件中的配置參數和初始驗證文件中參數之間的對應關系；

按照所述預設映射關系將所述任務流的配置文件中的配置信息映射為初始驗證文件中的參數，得到所述目標驗證文件。

3.根據權利要求2所述的方法，其特征在于，按照所述預設映射關系將所述任務流的配置文件中的配置信息映射為初始驗證文件中的參數包括：

將所述任務流的變量信息映射為初始驗證文件中的變量信息；

將所述變量信息的初始參數映射為初始驗證文件中的初始狀態信息；

將所述變量信息的狀態變更信息映射為初始驗證文件中的操作信息；

將所述任務流的驗證要求映射為初始驗證文件中的驗證條件信息。

4.根據權利要求1至3中任一項所述的方法，其特征在于，基于所述目標驗證文件對所述任務流的時序狀態進行形式化驗證包括：

調用所述目標驗證文件的模型檢測程序，以通過所述模型檢測程序運行所述目標驗證文件，以利用運行之后的所述目標驗證文件對所述任務流的時序狀態進行形式化驗證。

5.根據權利要求1所述的方法，其特征在于，所述方法還包括：

獲取所述任務流的初始配置文件；

在所述初始配置文件中添加所述至少一種配置信息，得到所述任務流的配置文件。

6.根據權利要求1所述的方法，其特征在于，基于所述目標驗證文件對所述任務流的時序狀態進行形式化驗證包括：

利用所述任務流的變量信息、所述變量信息的初始參數和所述變量信息的狀態變更信息，驗證所述任務流的時序狀態是否滿足所述驗證條件。

7.一種形式化任務驗證裝置，其特征在于，包括：

獲取單元，用于獲取待驗證任務的任務流的配置文件，其中，所述任務流的配置文件中包含以下至少一種配置信息：任務流的變量信息，所述變量信息的初始參數，所述變量信息的狀態變更信息，所述任務流的驗證條件；

構建單元，用于基于所述任務流的配置文件中所包含的配置信息構建目標驗證文件，其中，所述目標驗證文件為基于形式化驗證語言構建的文件；

驗證單元，用于基于所述目標驗證文件對所述任務流的時序狀態進行形式化驗證；

構建單元還用于：

利用解析關鍵字對所述任務流的配置文件進行解析，得到所述至少一種配置信息；解析關鍵字為：變量、初始參數、任務、狀態變更和驗證條件；

利用所述形式化驗證語言對所述至少一種配置信息進行編譯，得到所述目標驗證文件。

8.一種電子設備，包括存儲器、處理器及存儲在所述存儲器上并可在所述處理器上運行的計算機程序，其特征在于，所述處理器執行所述計算機程序時實現上述權利要求1至6中任一項所述的方法的步驟。

9.一種具有處理器可執行的非易失的程序代碼的計算機可讀介質，其特征在于，所述程序代碼使所述處理器執行上述權利要求1至6中任一項所述的方法的步驟。