形式化方法的工程化

作者 |張志鵬上海控安可信軟件創(chuàng)新研究院研發(fā)工程師

版塊 |鑒源論壇 · 觀模

01背 景

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

02形式化方法工程化面臨的挑戰(zhàn)

形式化驗(yàn)證技術(shù)發(fā)展至今，有著三種較為成熟的方法，其基本原理以及特點(diǎn)如表1所示：

表1形式化方法

傳統(tǒng)的形式化方法自動(dòng)化程度較低且理論性較強(qiáng)，在實(shí)際應(yīng)用中利用其直接進(jìn)行形式化驗(yàn)證存在著不小的障礙。目前隨著模型驅(qū)動(dòng)開發(fā)以及形式驗(yàn)證工具的發(fā)展，形式化驗(yàn)證的自動(dòng)化程度得到了顯著的提高。

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

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

03形式化方法工程化實(shí)例

調(diào)度系統(tǒng)從需求到源碼實(shí)現(xiàn)分為三個(gè)部分：需求規(guī)范、架構(gòu)設(shè)計(jì)和源代碼。為保證對調(diào)度系統(tǒng)的充分驗(yàn)證，基于模型檢測、SAT/SMT solver、CSP、Hoare邏輯等技術(shù)對這三部分均進(jìn)行了形式化建模和相應(yīng)的形式化驗(yàn)證。需求規(guī)范部分進(jìn)行了形式化需求轉(zhuǎn)換，并依據(jù)形式化需求和系統(tǒng)架構(gòu)獲得設(shè)計(jì)模型。而后使用形式化驗(yàn)證工具VCC、CBMC和PAT分別從單元級、模塊級和系統(tǒng)設(shè)計(jì)級對系統(tǒng)構(gòu)建的模型進(jìn)行形式化驗(yàn)證。

3.1 調(diào)度系統(tǒng)的形式化建模

形式化建模主要是根據(jù)調(diào)度系統(tǒng)的需求文檔和架構(gòu)設(shè)計(jì)來定義系統(tǒng)的CSP模型。首先是對調(diào)度系統(tǒng)需求的形式化建模，流程如圖2所示：

圖2 需求形式化建模流程

● 在底層需求的基礎(chǔ)上進(jìn)行需求的精化得到形式化需求；

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

● 針對功能需求構(gòu)建出系統(tǒng)模型，其中每條功能需求邏輯都在系統(tǒng)模型的進(jìn)程中進(jìn)行了詳細(xì)描述；

● 針對非功能需求構(gòu)建出其語義等價(jià)的模型約束；

● 將系統(tǒng)模型和性質(zhì)結(jié)合構(gòu)成整個(gè)形式化需求的需求模型。

在系統(tǒng)建模階段，需要對底層需求描述的內(nèi)容人工轉(zhuǎn)化為形式化需求，在此過程中對系統(tǒng)需求進(jìn)行進(jìn)一步精化和建模，便于后續(xù)的工具進(jìn)行相應(yīng)的分析與驗(yàn)證工作。

然后根據(jù)調(diào)度系統(tǒng)的架構(gòu)設(shè)計(jì)得到的任務(wù)狀態(tài)遷移模型如下圖3所示，使用CSP語言來描述系統(tǒng)行為。使用CSP對該模型采用如下建模步驟：

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

（2）描述各個(gè)進(jìn)程內(nèi)任務(wù)行為；

（3）描述進(jìn)程轉(zhuǎn)換信息；

（4）定義驗(yàn)證目標(biāo)。

圖3任務(wù)狀態(tài)遷移模型

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

3.2 調(diào)度系統(tǒng)的形式化驗(yàn)證

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

源代碼驗(yàn)證模塊：在驗(yàn)證了調(diào)度系統(tǒng)內(nèi)所有的單元的函數(shù)和子模塊后，發(fā)現(xiàn)了許多測試不能發(fā)現(xiàn)的類型不匹配、變量溢出、除0錯(cuò)誤、分支不可達(dá)、數(shù)組越界、指針內(nèi)存安全性等問題。

系統(tǒng)設(shè)計(jì)驗(yàn)證：調(diào)度系統(tǒng)應(yīng)該滿足任務(wù)間調(diào)度的無死鎖，且在中斷情況下的正確執(zhí)行。待驗(yàn)證的性質(zhì)主要包含以下三條：

（1）對于任務(wù)調(diào)度的無死鎖，使用PAT中提供的deadlockfree性質(zhì)來驗(yàn)證；

（2）對于任務(wù)調(diào)度的安全性性質(zhì)，這里定義為在任意時(shí)刻，只有一個(gè)任務(wù)處于運(yùn)行狀態(tài)；

（3）對于任務(wù)調(diào)度的活性性質(zhì)，滿足調(diào)度系統(tǒng)的優(yōu)先級執(zhí)行原則，不會(huì)出現(xiàn)優(yōu)先級反轉(zhuǎn)。

驗(yàn)證結(jié)果如下圖4所示：

圖4 PAT驗(yàn)證結(jié)果

在模擬了1147592狀態(tài)后，

（1）系統(tǒng)無死鎖性質(zhì)驗(yàn)證通過；

（2）系統(tǒng)未能夠執(zhí)行到同時(shí)有兩個(gè)任務(wù)處于運(yùn)行狀態(tài)錯(cuò)誤狀態(tài)，系統(tǒng)的安全性性質(zhì)滿足；

（3）系統(tǒng)未能夠執(zhí)行到優(yōu)先級反轉(zhuǎn)的錯(cuò)誤狀態(tài)，因此系統(tǒng)的活性性質(zhì)得到滿足。

若存在調(diào)度系統(tǒng)的遷移關(guān)系發(fā)生改變等異常情況時(shí)，PAT也能驗(yàn)證出調(diào)度系統(tǒng)的錯(cuò)誤，并給出錯(cuò)誤的路徑實(shí)例，存在死鎖的驗(yàn)證結(jié)果如下圖5所示：

圖5 PAT死鎖驗(yàn)證結(jié)果

04總 結(jié)

經(jīng)過調(diào)度系統(tǒng)的形式化驗(yàn)證發(fā)現(xiàn)了調(diào)度系統(tǒng)實(shí)現(xiàn)過程中的部分問題，源代碼模塊的問題是真實(shí)存在的問題，在某個(gè)函數(shù)或某個(gè)模塊的代碼實(shí)現(xiàn)中，該函數(shù)或模塊的輸入依賴于其他部分的傳遞，可能真實(shí)的場景下不會(huì)發(fā)生上述問題，但形式化驗(yàn)證可以發(fā)現(xiàn)這些測試發(fā)現(xiàn)不了的錯(cuò)誤。系統(tǒng)設(shè)計(jì)驗(yàn)證模塊可以發(fā)現(xiàn)系統(tǒng)設(shè)計(jì)中存在缺陷的地方，可以驗(yàn)證系統(tǒng)設(shè)計(jì)需要滿足的各種性質(zhì)，并可以注入特殊情況性質(zhì)來驗(yàn)證系統(tǒng)設(shè)計(jì)的完備性與安全性，存在錯(cuò)誤時(shí)，查看具體的錯(cuò)誤路徑來改善系統(tǒng)設(shè)計(jì)架構(gòu)。

綜上所述，形式化工程方法，就是以軟件形式化方法理論為基礎(chǔ)，以系統(tǒng)化的工程方法引導(dǎo)工業(yè)界工程人員構(gòu)建高質(zhì)量的軟件模型，用以引導(dǎo)后續(xù)的代碼編寫和相關(guān)測試分析。并選取了工業(yè)實(shí)際場景中的某操作系統(tǒng)的調(diào)度系統(tǒng)的形式化驗(yàn)證工作作為典型的形式化方法的工程化案例，應(yīng)用了形式化方法的需求分析、建模與驗(yàn)證，由此驗(yàn)證了形式化方法的可行性與有效性。

參考文獻(xiàn)：

[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].軟件學(xué)報(bào),2019,(01):33-61[37].

審核編輯黃宇