作者 |張志鵬上海控安可信軟件創新研究院研發工程師

版塊 |鑒源論壇 · 觀模

01背 景

形式化方法是基于嚴格的數學基礎，通過采用數學邏輯證明來對計算機軟硬件系統進行建模、規約、分析、推理和驗證，是用于保證計算機系統正確性以及安全性的一種重要方法。經典的形式化語言和相應的建模方法有VDM[1]、Z[2]、Object-Z[3]、B[4]、Event-B[5]、TLA+[6]，在軟件工程領域確立了較大的影響力且有較成功工業界應用。如Event-B曾成功用于巴黎地鐵的設計與開發，Amazon也將 TLA+用于Web Services的設計與開發。盡管形式化方法已經通過這些案例表現出了巨大潛力，但是由于對大型嵌入式控制軟件進行形式化規約的構建過于復雜，以及開發成本過高等問題，難以在工業界進行規模化的應用。其根本性的難點在于缺少一套將形式化方法與軟件工程有機融合，并能夠對其進行形式化建模的工程方法，引導工程人員從原始的以自然語言描述的需求出發，適應軟件需求變更等常見情況，逐步構建精確描述系統功能的形式化需求規約，并提供相應技術實施需求確認以保證需求規約充分而準確地刻畫了期望的功能。

02形式化方法工程化面臨的挑戰

形式化驗證技術發展至今，有著三種較為成熟的方法，其基本原理以及特點如表1所示：

表1形式化方法

傳統的形式化方法自動化程度較低且理論性較強，在實際應用中利用其直接進行形式化驗證存在著不小的障礙。目前隨著模型驅動開發以及形式驗證工具的發展，形式化驗證的自動化程度得到了顯著的提高。

“基于模型的軟件開發方法”作為一個嶄新的技術，使用如圖1所示的“Y”型開發流程。在其開發周期中，工程人員將模型作為核心，從而可以更加關注設計與需求的本身，同時在設計時可以對所建立的模型進行仿真測試，以盡早發現所存在的問題。并且針對設計到編碼實現的過程，可以由代碼自動生成技術完成，有效地降低引入人工錯誤的可能。

在基于模型的開發方法中，建模語言和建模工具是其最重要的支柱。而形式化方法則能提供建模語言與建模工具的支持。形式化方法被認為是保證軟件需求質量的重要手段，主要思想是建立形式化規約，用形式化規約語言精確地描述用戶對軟件的需求，通過對規約的逐步精化和驗證得到可信的軟件系統[7,8]。形式方法包含兩項重要技術：形式化規約（formal specification）與形式化驗證（formal verification）。前者關心的是形式化建模，即關注如何用精確的、無二義性的數學語言來書寫形式化規約用以描述軟件需求。后者根據數學方法例如定理證明或模型檢驗（model checking）等手段，對已建立的形式化規約進行分析，確認其是否滿足期望的性質，最大程度地發現需求模型中不一致和二義性等錯誤，從而根本上保證軟件的可靠性[9]。下面以一個工業中的具體案例來介紹形式化方法在實際中的應用場景，使用形式化建模驗證和形式化驗證工具來驗證某操作系統的調度系統安全性。

03形式化方法工程化實例

調度系統從需求到源碼實現分為三個部分：需求規范、架構設計和源代碼。為保證對調度系統的充分驗證，基于模型檢測、SAT/SMT solver、CSP、Hoare邏輯等技術對這三部分均進行了形式化建模和相應的形式化驗證。需求規范部分進行了形式化需求轉換，并依據形式化需求和系統架構獲得設計模型。而后使用形式化驗證工具VCC、CBMC和PAT分別從單元級、模塊級和系統設計級對系統構建的模型進行形式化驗證。

3.1 調度系統的形式化建模

形式化建模主要是根據調度系統的需求文檔和架構設計來定義系統的CSP模型。首先是對調度系統需求的形式化建模，流程如圖2所示：

圖2 需求形式化建模流程

● 在底層需求的基礎上進行需求的精化得到形式化需求；

● 將形式化需求基于類型進行功能需求和非功能需求的劃分；

● 針對功能需求構建出系統模型，其中每條功能需求邏輯都在系統模型的進程中進行了詳細描述；

● 針對非功能需求構建出其語義等價的模型約束；

● 將系統模型和性質結合構成整個形式化需求的需求模型。

在系統建模階段，需要對底層需求描述的內容人工轉化為形式化需求，在此過程中對系統需求進行進一步精化和建模，便于后續的工具進行相應的分析與驗證工作。

然后根據調度系統的架構設計得到的任務狀態遷移模型如下圖3所示，使用CSP語言來描述系統行為。使用CSP對該模型采用如下建模步驟：

（1）定義模型所需的變量和常量；

（2）描述各個進程內任務行為；

（3）描述進程轉換信息；

（4）定義驗證目標。

圖3任務狀態遷移模型

圖中顯示了調度系統的六種任務狀態，包括Ready（就緒態），Running（運行態），Int（中斷態），Suspend（掛起態），Dormant（睡眠態），Null（空狀態）。其中Null空狀態是任務在任務模塊初始化后的狀態，任務被創建后由空狀態遷移到Dormant睡眠態。任務創建完畢開始執行調度，睡眠態的任務可以遷移到Ready就緒態進入就緒隊列等待調度執行，進而遷移到Running運行態；或者被掛起遷移到Suspend掛起態；處于運行態的任務若被高優先級的任務搶占會遷到Int中斷態；而所有其他任務狀態在運行任務刪除調用后，都會返回到Dormant睡眠狀態。

3.2 調度系統的形式化驗證

為了保證驗證的充分性，使用VCC、CBMC對源代碼進行形式化驗證分析從而驗證系統源代碼的準確性與一致性。使用PAT工具對系統設計需求進行建模，驗證系統中的死鎖、活性等安全性質，并根據來自高層需求中的性質驗證系統設計需求是否滿足高層需求。驗證結果如下：

源代碼驗證模塊：在驗證了調度系統內所有的單元的函數和子模塊后，發現了許多測試不能發現的類型不匹配、變量溢出、除0錯誤、分支不可達、數組越界、指針內存安全性等問題。

系統設計驗證：調度系統應該滿足任務間調度的無死鎖，且在中斷情況下的正確執行。待驗證的性質主要包含以下三條：

（1）對于任務調度的無死鎖，使用PAT中提供的deadlockfree性質來驗證；

（2）對于任務調度的安全性性質，這里定義為在任意時刻，只有一個任務處于運行狀態；

（3）對于任務調度的活性性質，滿足調度系統的優先級執行原則，不會出現優先級反轉。

驗證結果如下圖4所示：

圖4 PAT驗證結果

在模擬了1147592狀態后，

（1）系統無死鎖性質驗證通過；

（2）系統未能夠執行到同時有兩個任務處于運行狀態錯誤狀態，系統的安全性性質滿足；

（3）系統未能夠執行到優先級反轉的錯誤狀態，因此系統的活性性質得到滿足。

若存在調度系統的遷移關系發生改變等異常情況時，PAT也能驗證出調度系統的錯誤，并給出錯誤的路徑實例，存在死鎖的驗證結果如下圖5所示：

圖5 PAT死鎖驗證結果

04總 結

經過調度系統的形式化驗證發現了調度系統實現過程中的部分問題，源代碼模塊的問題是真實存在的問題，在某個函數或某個模塊的代碼實現中，該函數或模塊的輸入依賴于其他部分的傳遞，可能真實的場景下不會發生上述問題，但形式化驗證可以發現這些測試發現不了的錯誤。系統設計驗證模塊可以發現系統設計中存在缺陷的地方，可以驗證系統設計需要滿足的各種性質，并可以注入特殊情況性質來驗證系統設計的完備性與安全性，存在錯誤時，查看具體的錯誤路徑來改善系統設計架構。

綜上所述，形式化工程方法，就是以軟件形式化方法理論為基礎，以系統化的工程方法引導工業界工程人員構建高質量的軟件模型，用以引導后續的代碼編寫和相關測試分析。并選取了工業實際場景中的某操作系統的調度系統的形式化驗證工作作為典型的形式化方法的工程化案例，應用了形式化方法的需求分析、建模與驗證，由此驗證了形式化方法的可行性與有效性。

參考文獻：

[1]JPL, NASA. Formal methods guidebook –nasa. http://eis.jpl.nasa.gov/quality/Formal Methods/.

[2]Hall, Using Formal Methods to Develop an ATC Information System, IEEE Software, vol. 13, no. 2, Mar., pp. 66-76, 1996.

[3]C. Jones, Systematic Software Development Using VDM. Prentice Hall, Second Edition, 1990.

[4]J.M.Spivey, The Z Notation: A Reference Manual. Prentice Hall International (UK) Ltd, Second Edition, 1998.

[5]G.Smith. The Object-Z Specification Language. Advancesin Formal Methods, Kluwer Academic, 2000.

[6]Chaudhuri K, Doligez D, Lamport L, et al. Verifying Safety Properties With the TLA+ Proof System[J]. Lecture Notes in Computer Science, 2010, 6173:142-148.

[7]METEOR-S: Semantic Web Services and Processes, http://lsdis.cs.uga.edu/proj/meteor/, 2015.

[8]Paradkar et al., Automated functional conformance test generation for semantic web services, IEEE Int. Conf. Web Services (2007) pp. 110–117.

[9]王戟,詹乃軍,馮新宇,等.形式化方法概貌[J].軟件學報,2019,(01):33-61[37].

審核編輯黃宇