[發明專利]發動機的控制軟件的形式化處理方法和裝置

在審

• 申請號: 202011373919.7
• 申請日: 2020-11-30
• 公開（公告）號: CN114579084A
• 公開（公告）日: 2022-06-03
• 發明（設計）人: 趙旭東;徐靜
• 申請（專利權）人: 中國航發商用航空發動機有限責任公司
• 主分類號: G06F8/10
• 分類號: G06F8/10;G06F8/35;G06F30/20
• 代理公司: 中國貿促會專利商標事務所有限公司 11038
• 代理人: 張海強

本公開提供了一種發動機的控制軟件的形式化處理方法和裝置，涉及形式化技術領域，所述方法包括：接收用戶輸入的所述控制軟件的半形式化的控制需求；根據定義的形式化語言，將所述半形式化的控制需求形成為形式化的控制需求；根據所述發動機的控制安全規則，對所述形式化的控制需求進行驗證；將驗證后的所述形式化的控制需求轉換為建模腳本，其中，所述建模腳本被配置為在被建模軟件執行后生成所述控制軟件的仿真模型。

技術領域

本公開涉及形式化技術領域，尤其是一種發動機的控制軟件的形式化處理方法和裝置。

背景技術

航空發動機的控制系統的安全性和可靠性有著非常嚴格的要求，例如，失效概率要求不高于10^-9/飛行小時。例如，民用航空發動機的控制可以采用全權限數字電子控制(FADEC)技術，其核心功能通過控制軟件來實現。

控制軟件具有大規模、高安全性和高成本的特點，先進的航空發動機的控制軟件的代碼量都是在百萬行的量級。由于軟件測試的不確定性以及復雜邏輯失效概率難以精確量化等原因，缺乏有效的確定性的方法對軟件的安全性進行度量。

軟件需求是軟件產品開發過程中的關鍵輸入。在發動機控制領域，控制軟件的需求通常為自然語言描述的文檔，對需求的確認往往采用行業專家人工核查的方法，但是這種方法往往只能給出定性的結論，主觀性較強，當驗證功能和結構復雜的發動機控制軟件時，具有較大的局限性。

隨著形式化方法的不斷發展，逐漸采用自動化的方法對控制軟件的需求進行定量的驗證，以在研發的早期階段及時發現和解決需求中存在的問題，提高軟件研發的效率。

軟件形式化方法是建立在嚴格數學基礎上的軟件開發方法，邏輯、代數、自動機、圖論等構成了形式化方法的數學基礎。形式化方法以及相應的形式化語言往往晦澀難懂，要求使用者具有很強的數學功底，普通工程師難以掌握該方法。并且，由于形式化方法的嚴格語義要求，使得在實際工程或技術領域，難以覆蓋全部技術要求，通常只能在單個、有限的范圍內進行應用。

發明內容

發明人注意到，相關技術中，形式化方法往往與軟件開發方法之間割裂開來。傳統的控制軟件的開發流程基于文檔化的控制軟件的需求，工程師通過閱讀需求在建模軟件等工具上建立控制軟件的仿真模型，通過建模軟件的自動代碼生成工具生成嵌入式代碼，經過一系列的測試驗證之后完成整個軟件的開發工作。

形式化方法往往基于特定的形式化語言和工具，只能實現單一的驗證工作，其建立的形式化模型往往單獨存在而不能繼續利用，與軟件開發流程體系之間沒有很好的融合。

有鑒于此，本公開實施例提出了如下技術方案。

根據本公開實施例的一方面，提供一種發動機的控制軟件的形式化處理方法，包括：接收用戶輸入的所述控制軟件的半形式化的控制需求；根據定義的形式化語言，將所述半形式化的控制需求形成為形式化的控制需求；根據所述發動機的控制安全規則，對所述形式化的控制需求進行驗證；將驗證后的所述形式化的控制需求轉換為建模腳本，其中，所述建模腳本被配置為在被建模軟件執行后生成所述控制軟件的仿真模型。

在一些實施例中，所述接收用戶輸入的所述控制軟件的半形式化的控制需求包括：響應于用戶輸入的多個變量，對所述多個變量進行檢查，以使得所述多個變量的名稱彼此不同；響應于用戶輸入的多個功能任務和所述多個功能任務對應的彼此不同的多個編號，對每個功能任務進行檢查，以使得每個功能任務中的每個變量均屬于所述多個變量；響應于用戶輸入的多個控制狀態的調用邏輯，對每個控制狀態的調用邏輯進行檢查，以使得每個控制狀態調用的每個功能任務的編號均屬于所述多個編號；接收用戶輸入的狀態遷移邏輯和時序控制邏輯，所述狀態遷移邏輯包括所述控制軟件需要的不同控制狀態之間的遷移順序，所述時序控制邏輯包括所述控制軟件需要的每個控制狀態調用的每個功能任務的持續時間。