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

王明亮 王永 尤志堅 施敏華

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

關(guān)鍵詞：星載軟件;形式化驗證;需求規(guī)約化;形式化語法

中圖分類號：TP311文獻標(biāo)識碼：A

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

1概述

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

2形式化方法研究動態(tài)

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

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

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

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

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

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

1）根據(jù)航天領(lǐng)域的特征提取系統(tǒng)功能和行為特征，給出需求模板背后的形式化語法和語義，制定對應(yīng)的需求模板。

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

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

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

5 結(jié)束語

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

參考文獻：

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

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

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

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

【通聯(lián)編輯：梁書】