雖然在軟件開發(fā)周期中創(chuàng)建形式化的模型已經(jīng)有明顯的好處，但是形式化方法的最大優(yōu)勢在于對這些模型進行的形式化分析。形式化分析可以提供軟件屬性和軟件符合需求的保證(guarantees)或證據(jù)(proofs)。提供保證或證據(jù)意味著所有可能的運行情況都被考慮在內(nèi)，即完備性。為了進行形式化分析，一組軟件屬性是必要的。這些屬性可以被創(chuàng)建出來，也可以被嵌入到要實現(xiàn)形式化分析的特定工具中(例如，最壞運行時間分析)。形式化分析的屬性在許多方面可以被視為類似于可驗證的測試需求。在測試中，測試用例應(yīng)該很容易從可驗證的需求中導(dǎo)出，對于形式化分析，屬性通常也是待驗證的測試用例。可以為一組需求定義一組完整的屬性，在這種情況下，該組屬性集總是成立的證據(jù)，證明了所分析的模型與其需求的等價性。

值得一提的是，僅當對屬性的確定性分析是堅實可靠的分析，才可稱為形式化分析。堅實可靠的分析意味著：當一個屬性可能不為“真”時，形式化方法從不斷言它為“真”。相反，斷言一個可能是“真”的屬性為“假”時，則是可以接受的。因為這是一個可用性的問題，而不是可靠性的問題。通俗地講，引起“產(chǎn)生錯誤的警報”是允許的。此外，在試圖證明屬性是否成立時，形式化方法的結(jié)果返回“不知道”或者不返回結(jié)論也是可以接受的。在這種情況下，就需要額外的驗證(精化屬性、調(diào)整分析引擎等)。

因為形式化的方法=形式化模型+形式化分析，所以軟件行業(yè)內(nèi)絕大部分基于模型的開發(fā)工具，如果不做專門的定制或轉(zhuǎn)換，由于模型本身不是形式化的，也就無從談起形式化的方法。而SCADE由于其支撐語言發(fā)軔于形式化的語言Lustre等，SCADE是主流商業(yè)工具里唯一的、真正的、形式化的模型，再結(jié)合第三方形式化分析引擎(Prover，S3，SafeProver，GATel等)，在不同行業(yè)已經(jīng)得到較多形式化方法驗證的成功案例。

上述提到的《DO-333》文檔中標識了三類典型的形式化分析，其定義分別如下：

抽象解釋Abstract Interpretation（也有稱之為靜態(tài)分析Static Analyzer）: 定義構(gòu)造一個編程語言語義的保守表示，用于“有限狀態(tài)程序的動態(tài)屬性的合理確定……它可以被看成一個計算機程序的部分執(zhí)行，它確定了程序的特定效果(例如，控制結(jié)構(gòu)、信息流、堆棧大小、時鐘周期數(shù))，而不實際執(zhí)行所有的計算”。

抽象解釋的方法相對簡單，可用靜態(tài)分析工具檢查除0(division-by-zero)，越界(out of bound array access)，溢出(Overflows)等問題，但可能產(chǎn)生虛假警告。

相關(guān)的主流商業(yè)工具有AbsInt的Astree，Mathworks的Polyspace Code Prover和TrustInSoft的TrustInSoft Analyzer。

模型檢查Model checking：搜索一個形式化模型的所有行為，以確定一個指定的屬性是否滿足。

模型檢查用于判定系統(tǒng)的形式化模型是否滿足基于規(guī)約(Specification)的正確屬性。模型檢查通常有三個結(jié)果：1. 屬性正確；2屬性錯誤，并給出反例；3. 分析超時 (TO: Time Out) 無法確定。相對于抽象解釋，模型檢查可提供了安全屬性的更好的表現(xiàn)形式。然而由于對非線性算法，狀態(tài)組合空間爆炸等處理能力的不足，其使用范圍也受限制。對工程師而言，模型檢查最大的價值在于當安全屬性違反后，會自動生成反例。當安全屬性無法驗證時，它能顯示導(dǎo)致該錯誤狀態(tài)的運行記錄。

相關(guān)的主流商業(yè)工具有Kind2 (University of Iowa) ，JKind (Rockwell Collins) ，CEA的GATeL和Prover Technologies 的Design Verifier等。

演繹法Deductive proof：使用數(shù)學(xué)論證來建立一個形式化模型的每個屬性。通常使用一個理論證明工具來構(gòu)造證明，以顯示軟件屬性是成立的。

演繹法是使用數(shù)學(xué)參數(shù)來判定每個形式化模型的屬性，最終目標是定理證明(Theorem Proving)，證明通常是基于Hoare邏輯和Dijkstra先決條件推理。相對于抽象解釋和模型檢查，演繹法是更有效的。然而該方法通常要求非常專業(yè)的人員參與，自動化程度較低，即使很普通的推理驗證也經(jīng)常需要耗費數(shù)周甚至上月的時間，難以在大規(guī)模的項目上應(yīng)用，甚至在某些情況下是根本不可能使用的。相關(guān)的主流工具有STeP(Standford Theorem Prover)、ACL2 、HOL 、PVS 、TLV 、Coq等。

以上三類形式化分析具有一些共性。首先，它們都依賴于形式化的模型。非形式化模型，或非形式化模型和形式化模型混合的復(fù)合模型都不足用形式化的方法來表明規(guī)約和代碼之間的符合性，所以要求必須是真正的形式化的模型。第二，所有的形式化分析通常都是用一個工具實現(xiàn)的。

下圖是形式化分析的全景圖，可見三種方法的自動化程度和可處理的代碼量由高到低排列，但安全屬性證明的完備性由低到高排列。

根據(jù)Xavier Leroy改寫的形式化方法全景圖

三種形式化方法中抽象解釋和模型檢查的工程實踐應(yīng)用較為廣泛，SCADE中也早已經(jīng)內(nèi)嵌了基于抽象解釋和模型檢查兩種技術(shù)的形式化分析工具(屬于AbsInt公司和Prover公司等)。抽象解釋一般可通過簡單的按鈕操作進行標準化的分析來快速得出結(jié)果，對此就不作進一步描述了；而模型檢查結(jié)果的得出還是有些工作量的，部分復(fù)雜項目可能還會耗費工程師們不少功夫才能成功應(yīng)用。下面就對模型檢查進行展開介紹。

模型檢查作為一種包含了一系列面向有限狀態(tài)系統(tǒng)驗證技術(shù)的框架，最早由Clarke、Emerson、Quielle和Sifakis在1981年分別提出，他們中的部分人也因此獲得了2007年的圖靈獎。

部分圖靈獎獲得者在形式化驗證方面的研究

模型檢查方法主要通過遍歷系統(tǒng)的有窮狀態(tài)空間以驗證系統(tǒng)是否滿足某些關(guān)鍵的系統(tǒng)屬性。模型檢查的輸入通常為兩個，以自動機(automata)模型描述的系統(tǒng)和以時序邏輯公式(temporal logic formula)描述的系統(tǒng)屬性。其中模型實現(xiàn)了系統(tǒng)的行為，屬性描述了系統(tǒng)應(yīng)該做什么、或者不應(yīng)該做什么。

模型檢查的方法

系統(tǒng)模型和待驗證的屬性都需要以高度抽象和精確嚴密的方式進行描述。近年來學(xué)術(shù)界以混成系統(tǒng)(Hybrid System)的概念來描述工業(yè)界安全關(guān)鍵領(lǐng)域的嵌入式系統(tǒng)，其特點是系統(tǒng)的行為里既包含連續(xù)的時間行為(可用微分方程描述的流表示)，又包含離散的邏輯控制(可用狀態(tài)機或自動機描述的跳轉(zhuǎn)表示)，而且連續(xù)的時間行為和離散的邏輯控制并不相互獨立，而是糅合交織在一起的，共同構(gòu)成描述真實系統(tǒng)的復(fù)雜邏輯。從此前《細數(shù)Ansys SCADE的前世今生》一文可以看出，SCADE是從工業(yè)界的真實應(yīng)用推動而發(fā)展起來的，它恰是包含了微分方程、狀態(tài)機和自動機等多種形式化語言的融合產(chǎn)物，可以滿足混成系統(tǒng)的要求。因此，SCADE是形式化方法中實現(xiàn)系統(tǒng)模型的較好工具之一。

而屬性描述語言通常是用時序邏輯公式(temporal logic formula)。時序邏輯公式是一種為涉及時間的陳述和推理而量身定制的數(shù)學(xué)形式，相當接近自然語言，它還附帶了形式化語義。常見的時序邏輯公式是線性時間邏輯(LTL: Linear Temporal Logic)和計算樹邏輯(CTL: Computation Tree Logic)。LTL和CTL的組合稱為CTL*。

迄今為止，模型檢查的算法大致發(fā)展了三代。

第一代是顯式/狀態(tài)模型檢查(Explicit/state model checking)方法，它可以顯式地探索模型的狀態(tài)空間，并通過正向探索進行搜索，直到發(fā)現(xiàn)屬性沖突。該方法對于LTL和CTL提出了不同的思路。在LTL模型檢查中，探索算法可以是深度優(yōu)先(depth-first)或廣度優(yōu)先(breadth-first)的：廣度優(yōu)先的方法可以找到最短的可能反例，但對內(nèi)存使用的要求明顯高于深度優(yōu)先的方法。在CTL模型檢查中，通過遞歸地計算每個狀態(tài)是否滿足的子公式，來確定滿足給定屬性的所有狀態(tài)集。如果所有的狀態(tài)都被訪問并且沒有檢測到違反，則判定該模型滿足該屬性。毫不意外，第一代模型檢查方法了就遇到了狀態(tài)空間爆炸問題。

第二代是符號模型檢查(symbolic model checking)方法，該方法使用一種稱為二元決策圖(BDD：Binary Decision Diagrams)的特殊數(shù)據(jù)結(jié)構(gòu)，可以更有效地表示狀態(tài)集和函數(shù)關(guān)系，從而允許表示更大的狀態(tài)空間。

第三代是有界模型檢查(BMC: Bounded Model Checking)方法，作為基于二元決策圖 (BDD: Binary Decision Diagram)的符號模型檢查的一種補充方法，有界模型檢查技術(shù)被學(xué)者提出并得到了廣泛的應(yīng)用。其主要思想是通過一個整數(shù)k來限制模型行為步數(shù)，將系統(tǒng)k步內(nèi)的行為編碼成一組布爾約束，然后基于SAT(Boolean Satisfiability)方法對其求解從而高效地找出k步內(nèi)的所有錯誤。雖然BMC方法因為只能驗證閾值內(nèi)的系統(tǒng)屬性而相對缺失了模型檢查的完備性，但是通過限定模型的行為步數(shù)，其在發(fā)現(xiàn)錯誤的能力上超越了傳統(tǒng)模型檢查方法。此外，由于BMC方法只需要遍歷閾值內(nèi)的系統(tǒng)狀態(tài)空間，使得其能處理的系統(tǒng)規(guī)模得到了提升，這也是BMC得到廣泛認可的優(yōu)勢所在。

不同于半自動化甚至全手動的定理證明，模型檢查可以自動執(zhí)行并能在系統(tǒng)不滿足屬性時給出相應(yīng)的錯誤信息，因此在工業(yè)界比其他形式化方法更受推崇。然而，由于模型檢查技術(shù)的較高復(fù)雜性，時至今日依然難以處理業(yè)界的大規(guī)模系統(tǒng)。由羅克韋爾柯林斯公司發(fā)布的報告可以看到，模型檢查技術(shù)對于非線性的、可達狀態(tài)空間小于10200的有限情況能作出有意義的分析。

Miller, Steven P關(guān)于模型檢查技術(shù)的可擴展驗證域圖

對SCADE模型進行形式化分析的絕大部分商用工具采用的就是基于BMC方法的模型檢查技術(shù)。當前SCADE 在2020 R1版本中包含了Prover Technology的Design Verifier引擎，Design Verifier引擎里內(nèi)置了SAT解算器，可以對SCADE模型進行模型檢查，當結(jié)果為錯誤時，自動給出反例的測試用例。

使用SCADE模型實現(xiàn)形式化驗證的通用方法是：保持原有設(shè)計模型不變，根據(jù)需求定義含安全屬性的觀察模型，再設(shè)計頂層操作符將設(shè)計模型和屬性觀察模型串聯(lián)起來，最終分析屬性模型的輸出即可。

SCADE模型檢查方法簡圖

基于SCADE模型的形式化方法詳細工作流如下。

SCADE模型的形式化方法工作流

1. 創(chuàng)建新的形式化驗證工程，或在當前開發(fā)工程中使能形式化分析引擎，這樣就能自動將形式化驗證相關(guān)的Suite預(yù)定義庫導(dǎo)入到工程中

2. 根據(jù)安全需求和使用場景定義觀察者模型，其中包含的安全屬性也是用Suite設(shè)計，該安全屬性的輸出必須設(shè)計為bool類型，以true值輸出代表安全導(dǎo)向，供形式化引擎進行分析

3. 創(chuàng)建頂層操作符，將原設(shè)計模型和觀察者/屬性模型連接起來。可以在頂層操作符中使用Assert功能添加約束，排除無關(guān)的場景，以加速形式化分析過程

4. 根據(jù)安全屬性創(chuàng)建自定義的形式化驗證目標，或直接啟用Suite內(nèi)置預(yù)定義的形式化驗證目標

5. 定制形式化驗證策略，并將策略應(yīng)用到形式化驗證目標上

6. 啟動形式化引擎進行分析

7. 輸出形式化驗證結(jié)果

8. 檢查結(jié)果，為真則得證，為假，則導(dǎo)入給出的反例進行模型仿真，再基于仿真結(jié)果修正模型后，迭代進行下一輪形式化分析

步驟4中指出的Suite內(nèi)置預(yù)定義的形式化驗證目標有4種

• 除0檢查：Division-by-Zero PO：驗證是否會引起除0的可能

• 溢出檢查：Overflow PO:驗證數(shù)值類型數(shù)據(jù)在賦值、移位或類型轉(zhuǎn)換時是否會溢出等

• 動態(tài)訪問檢查：Dynamic Access PO：驗證數(shù)組索引是否越界等

• 一致性檢查：Consistency PO: 驗證假設(shè)和約束是否一致，約束可以由Assume功能添加

SCADE形式化驗證面板

步驟5中指出的形式化驗證策略有如下3種：

SCADE形式化驗證策略

Debug策略和Induction策略中的屬性及其含義如下:

SCADE策略的屬性

SCADE Design Verifier選項卡與安全屬性策略

使用形式化驗證策略有助于用戶

• 在開發(fā)過程早期迅速查找bug

• 通過驗證某個獨立完整的需求對應(yīng)的安全屬性，證明需求是正確的

• 節(jié)省驗證成本，提高產(chǎn)品可信度

某項目的形式化分析頂層操作符的設(shè)計如圖表

SCADE某頂層操作符的設(shè)計

形式化分析的正確和錯誤的結(jié)果輸出如下圖所示

SCADE形式化正確或錯誤的分析結(jié)果

當形式化分析是錯誤時，可在詳細錯誤界面單擊超鏈接跳轉(zhuǎn)到該安全屬性。也可在配置正確的前提下，直接單擊Load Scenario直接導(dǎo)入反例給出的測試用例，進行白盒仿真。

SCADE形式化分析錯誤后導(dǎo)入反例進行白盒仿真

最后，可在SCADE程序中，或者工程目錄下查看每次分析后的Html格式的形式化驗證報告。

SCADE形式化分析的目錄級網(wǎng)頁格式報告

模型檢查用于判定系統(tǒng)的形式化模型是否滿足基于規(guī)約(Specification)的正確屬性。這是模型檢查的常規(guī)用法。有趣的是，也有不少學(xué)者的研究提出，可以使用模型檢查技術(shù)生成覆蓋分析相關(guān)的測試用例。該方法需要反向設(shè)計，故意設(shè)計一組“缺陷屬性”(trap properties)，該缺陷屬性聲稱: 某分支無論如何運行，都不可能被覆蓋的。如果模型檢查證明該“缺陷屬性”為假，就能得到反例，而反例就是可以覆蓋該分支的測試用例。數(shù)學(xué)上就是將上面描述的自動機進行非空檢測，且此時結(jié)果應(yīng)該為非空。

模型檢查生成測試用例

同模型檢查方法的正向使用一樣，對“缺陷屬性”的檢查也會遇到狀態(tài)空間爆炸的問題。在系統(tǒng)模型已經(jīng)確定的前提下，如何在盡可能短的時間內(nèi)，設(shè)計出恰當?shù)摹叭毕輰傩浴笔翘岣邷y試用例生成效率的關(guān)鍵。在后續(xù)文章中將介紹不同行業(yè)的客戶在項目中結(jié)合SCADE工具進行的形式化方法應(yīng)用。

本文結(jié)合機載軟件的適航標準第三版DO-178C的補充文檔《DO-333，DO-178C和DO-278A的形式化方法補充》介紹了基于SCADE模型的形式化方法。形式化方法=形式化模型+形式化分析。形式化方法主要分三類：抽象解釋、模型檢查和演繹法。SCADE是主流商業(yè)工具里唯一的、真正的、形式化的模型，可結(jié)合不同的第三方形式化分析引擎實現(xiàn)形式化方法。SCADE已內(nèi)嵌了基于抽象解釋和模型檢查兩種技術(shù)的形式化分析工具 (AbsInt公司和Prover公司等) 。

值得一提的是，Ansys與Honeywell在嵌入式系統(tǒng)領(lǐng)域已合作多年，未來將共同研發(fā)把Honeywell為航空項目而自研(in-house)的形式化驗證工具鏈Hi-Lite進行優(yōu)化改進，使其逐步成為SCADE的標準模塊。

[1] Leanna Rierson.安全關(guān)鍵軟件開發(fā)與審定——DO-178C標準實踐指南[M]. (崔曉峰). 北京：電子工業(yè)出版社，2015年6月

[2] Todorov V, Boulanger F, Taha S. Formal verification of automotive embedded software[C]//Proceedings of the 6th Conference on Formal Methods in Software Engineering. ACM, 2018: 84-87.

[3] Xavier Leroy Trust in compilers, code generators, and software verification tools [EB/OL].

[4] 宋俊. LTLNFBA: LTL 公式到 Büchi 自動機的轉(zhuǎn)換[D]. 西安電子科技大學(xué), 2014.

[5] 王瑞. 基于 SAT 的符號化模型檢驗技術(shù)研究[D]. 國防科學(xué)技術(shù)大學(xué), 2014.

[6] Sun Y. Strengthening fonctional validation of critical system by using Model Checking: Application to Instrumentation and Control systems in nuclear power plants[D]. 2017.

[7] Li W, Kan S, Huang Z. A Better Translation from LTL to Transition-Based Generalized Büchi Automata[J]. IEEE Access, 2017, 5: 27081-27090.

[8] 劉志鋒. 模型檢測中關(guān)鍵技術(shù)的研究及其應(yīng)用[D]. 南京大學(xué), 2011.

[9] 解定寶. 混成系統(tǒng)有界模型檢驗優(yōu)化技術(shù)研究[D]. 南京大學(xué), 2016.

[10] Miller S P. Bridging the gap between model-based development and model checking[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2009: 443-453.

[11] SCSDV_2019R1_M01_Tool. Ansys SCADE Suite Design Verifier and Formal Verification [EB/OL]. Ansys SBU. 2019（內(nèi)部文檔）

https://xavierleroy.org/talks/ERTS2018.pdf. Embedded Real Time Software and Systems, 2018-02-02

[12] Bhatt D, Madl G, Oglesby D, et al. Towards scalable verification of commercial avionics software[M]//AIAA Infotech@ Aerospace 2010. 2010: 3452.

[13] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of Formal Methods. Journal of Software, 2019, 30(1): 33-61(in Chinese). http://www.jos.org.cn/1000-9825/5652.htm

[14] 形式化方法導(dǎo)論[M]. 清華大學(xué)出版社 , 張廣泉, 2015