芻議面向航天器星載軟件的形式化驗證方法

王明亮 王永 尤志堅 施敏華

摘要：隨著星載軟件在航天器上實現的功能比重越來越高，星載軟件可靠性和可信性的指標要求越來越嚴格。傳統軟件測試方法的局限性難以確保萬無一失，形式化方法以其高度數學化和嚴謹性的特點，常被應用于安全關鍵軟件的驗證。本文針對星載軟件的高可靠性和充分性驗證需求，初步提出了相應的形式化驗證方案和需求建模實施過程，對于后續整星級的軟件驗證或者其他單機組件的驗證具有一定的參考和借鑒意義。

關鍵詞：星載軟件;形式化驗證;需求規約化;形式化語法

中圖分類號：TP311文獻標識碼：A

文章編號：1009-3044（2020）25-0205-02

1概述

星載軟件作為整個衛星的靈魂，由于實時性要求高、可靠性要求高、運行環境特殊、結構復雜等諸多特點，雖然經過單機對接測試、桌面聯試、整星模飛等多種測試，但是始終面臨需求分析嚴密性不足、測試充分性低下、邏輯設計錯誤等問題。特別地，傳統航天軟件以手工編碼為主，隨著軟件規模和復雜度的提升，進度的壓力使得保證需求分析和設計階段的全面性十分困難[1]。傳統測試方式難以從根本上改變和提高星載軟件可靠性，為了提高軟件質量，航天軟件工作者不停地在多個層面積極開展工作確保萬無一失，如制定并實施一系列航天軟件工程標準和規范、積極推進基于GJB5000A的軟件過程改進、對軟件進行大量的測試（單元測試、組裝測試、確認測試、系統測試、整星測試等）驗證盡可能多地暴露軟件問題，這些方法極大地減少了軟件錯誤的數量，保證了航天任務的成功。但盡管如此，軟件中的一些深層次的缺陷問題并不能在軟件測試中被全部識別，亟須采用更為嚴格的數學邏輯推理即形式化驗證的方法來提升和確保軟件的可靠度。

2形式化方法研究動態

形式化驗證通過對系統進行窮盡搜索來進行驗證，它以某個或某些形式的規范或屬性為依據，使用數學的方法證明其正確性[2]。Robert W. Floyd于1967年提出的最早的形式化方法之一公理化方法驗證程序的控制流，以及隨后TonyHoare在此基礎上繼續研究于1969年提出了程序驗證的公理系統Hoare邏輯;陳鋼博士在2016年3月的北京大學學報上發表了綜述性的文章對基于邏輯的各種形式化驗證方法和工具進行分析比較，可以幫助工程師從應用角度選擇使用驗證工具。清華大學賀飛博士等在軟件學報上開辟了軟件形式化驗證和形式化方法理論基礎專題，對最新錄用的國內外研究論文進行評價分析;丁明等提出了業務流程上的形式化設計和驗證方法;針對應答器報文編制規則黃旭等人給出了形式化建模與驗證方法;趙正旭等在2016年進行的Z規格說明的推理與驗證;查君鵬針對SPARCv8匯編程序進行了形式化驗證;部分圖靈獎獲得者也在形式化方面進行了一些研究工作，如下表所示[3]。

3 航天星載軟件形式化驗證技術方案

形式化方法是一種以數學基礎為設計理念，針對數字化系統進行規格說明撰寫、軟件開發、軟件驗證的技術，數學基礎包括形式邏輯，離散數學和機器可識別語言等。形式化模型是一種用數學語法和語義刻畫的模型，是一種對軟件諸多方面的抽象表達形式，用于后續的分析與驗證。應用形式化驗證方法的前提條件是對即將開發的軟件工程建立一個形式化全周期模型。

針對航天星載軟件的形式化驗證，首先要根據衛星分系統技術需求文檔建立形式化需求模型，然后對其進行分析與驗證，從而在軟件開發的早期發現并解決需求中存在的問題，諸如可達性錯誤，數據溢出超限，量綱錯誤，二義性錯誤等。基于驗證過的需求模型將其轉化為系統模型，在模型中驗證系統是否符合給定的安全性質，如順序性，完備性等。同時，利用模型動態檢查技術，在模型模擬執行時定位并發現代運行時錯誤，如并發性競爭等時序錯誤。針對驗證過的系統模型可以自動生成軟件代碼，但是因為現有的航天軟件大部分情況下均已存在經過嚴格測試的軟件代碼，一般不會直接使用生成的代碼，而是作為原有代碼的參考補充。同時，基于模型可以生成相對應的測試用例用于測試代碼，保障代碼的可靠性與安全性。星載軟件形式化驗證總體方案如圖1所示。

4 星載軟件形式化需求建模實施過程

在航天星載軟件的形式化需求建模過程中，首先需要使用系統化的過程控制引導需求分析者逐步完成從需求文檔到形式化模型轉換。在形式化需求模型建立階段，具體流程圖2所示，具體來說有以下三步：

1）根據航天領域的特征提取系統功能和行為特征，給出需求模板背后的形式化語法和語義，制定對應的需求模板。

2）根據需求模板，將原有的自然語言撰寫的非形式化需求文檔按照填充到模板中形成形式化需求文檔。填充模板的好處是不需要工程師學習形式化的數學語義便可以完成需求文檔的形式化轉換，其原有的工作流程不會受到影響。同時，在該過程中分析提取系統所需要驗證的安全性和可靠性性質，為后續的性質驗證提供輸入。

3）將形式化需求文檔作為工具的輸入，機器自動將其中的自然語言等非形式化內容全部過濾去除，得到由純形式化語言描述的需求模型，我們稱之為軟件的“原型”。

軟件需求分析位于軟件開發的前期，是軟件生存期中重要的一步[4]。由于在軟件起步階段，人們對系統預期功能尚不明確，而參與系統分析的人員背景不同，因此，采用自然語言完成初始的需求文檔顯然是個合理的方式。特別是對于航天星載軟件的需求來說，需求分析人員需要頻繁地與委托方進行方溝通交流，基于自然語言的非形式化需求規約在這個階段比形式化需求規約在可讀性和可理解性上有明顯的優勢。

5 結束語

形式化驗證在自頂向下的實現流程中增強了設計人員對系統的理解，能夠發現其他方法不易識別的設計缺陷，揭示系統設計中存在的不一致性、模糊和不完整性等問題。正如1996年IEEE會刊提出的觀點：“隨著軟件設計復雜度的不斷提高，形式化驗證將從實驗室走進生產領域”。形式化驗證理論研究雖然在學術上取得了一定成功，但是在工程落地方面還有很長的路要走。因為對于一般的軟件測試人員，在理解形式化推理演繹技術前，要先研究相對難度較高的形式化相關基礎數學推演理論，再嘗試將系統轉換為形式化模型形式化應用，帶來過高人力成本和難以接受的測試周期。但是，作為面向軟件正確性證明的最嚴格的基礎數學方法，軟件形式化驗證對軟件測試可信度和充分性的提升是毋庸置疑的。

參考文獻：

[1] 杜澤民.基于模型的軟件需求驗證方法研究[D].北京： 中國航天科技集團公司第一研究院， 2018.

[2] 于文濤.形式化驗證在軌道交通領域的應用[J].電腦知識與技術.2018，14（13）：263.

[3] 王戟、詹乃軍、馮新宇、劉志明.形式化方法概貌[J].軟件學報， 2019，30（1）： 33-61.

[4] 馬文姣. 航天型號軟件的安全性測試技術研究[D].哈爾濱： 哈爾濱工業大學， 2007.

【通聯編輯：梁書】