形式化方法概貌*

王 戟,詹乃軍,馮新宇,劉志明

1(國防科技大學 計算機學院,湖南 長沙 410073)

2(高性能計算國家重點實驗室(國防科技大學),湖南 長沙 410073)

3(中國科學院 軟件研究所,北京 100190)

4(天基綜合信息系統重點實驗室(中國科學院 軟件研究所),北京 100190)

5(南京大學 計算機科學與技術系,江蘇 南京 210023)

6(計算機軟件新技術國家重點實驗室(南京大學),江蘇 南京 210023)

7(西南大學 計算機與信息科學學院,重慶 400715)

8(西南大學 軟件研究與創新中心,重慶 400715)

計算機科學的發展主要涉及硬件和軟件的發展,而軟、硬件發展的核心問題之一是如何保證它們是可靠的、安全的,關鍵問題是正確性.如今,硬件性能變得越來越高、運算速度變得越來越快、體系結構變得越來越復雜,軟件的功能也變得越來越強大而復雜,如何開發可靠的軟、硬件系統,已經成為計算機科學發展的巨大挑戰.特別是現在計算機系統已廣泛應用于許多關系國計民生的安全攸關系統中,例如高速列車控制系統、航空航天控制系統、核反應堆控制系統、醫療設備系統等等,這些系統中的任何錯誤都可能導致災難性后果.

現代計算科學和計算機科學技術源自于Church的Lambda演算和Turing的圖靈機等計算模型.這些形式系統提供了計算的理論基礎.計算系統的設計開發需要分析、處理、證明計算機硬件和軟件系統的性質.形式化方法以形式(邏輯)系統為基礎,支持對計算系統進行嚴格的規約、建模和驗證,并且為此設計算法從而建立計算機輔助工具.在現代計算系統的開發過程中,形式化方法在不同的階段、以不同的形式和程度得以應用,例如:在基于模型的軟件開發中,建模、模型精化和基于模型的測試都是基于形式化方法的思想和技術發展起來的;程序語言的類型設計、程序分析的算法都是形式化方法中的基本技術.

形式化方法已經成功應用于各種硬件設計,特別是芯片的設計.各大硬件制造商都有一個非常強大的形式化方法團隊為保障系統的可靠性提供技術支持,例如IBM、Intel、AMD等等.由于軟件系統的復雜性和不確定性遠遠超出硬件系統,形式化方法在軟件開發中應用程度并不高.但是在最近 10多年中,隨著形式驗證技術和工具的發展,特別是在程序驗證中的成功應用,形式化方法在處理軟件開發復雜性和提高軟件可靠性方面已顯示出無可取代的潛力.各個著名的研究機構都已經投入大量人力和物力從事這方面的研究.例如,美國宇航局(NASA)擁有一支龐大的形式化方法研究團隊,他們在保證美國航天器控制軟件正確性方面發揮了巨大作用.在美國研發“好奇號”火星探測器時,為了提高控制軟件的可靠性和生產率,廣泛使用了形式化方法.微軟、華為、Synopsis、Facebook、Amazon等公司聘用形式化方法的專家從事形式驗證技術研究及工具開發工作,以期提高其商業軟件的可靠性.國際上已經出現了一批以形式化方法為核心競爭力的高科技公司,例如 Galois、Praxis等等.

本文主要給出形式化方法的基本方法學和發展概貌,第1節介紹形式化方法的基本概念、簡要歷史和構成體系.第2節、第3節分別介紹形式規約和開發以及形式驗證的基本內容和現狀.第4節介紹形式化方法的應用.第 5節討論形式化方法面臨的一些挑戰,展望其在軟件逐漸成為基礎設施時代的發展趨勢和交叉方向,并給出一些加強形式化教育的建議.

關于已有的介紹形式化方法的中文文章和報告,我們推薦文獻[1-3],其中,文獻[1]是關于形式化方法的最新進展的報告,而關于軟件分析的文獻[2,3]討論了面向程序或程序模型的形式化方法(包括模型檢驗、抽象解釋和符號執行)的新進展.

1 形式化方法基本概念

形式化方法是基于嚴格數學基礎,對計算機軟(硬)件系統進行形式規約、開發和驗證的技術.其中,形式規約使用形式語言構建所開發的軟件系統的規約,它們對應于軟件生命周期不同階段的制品,刻畫系統不同抽象層次的模型和性質,例如需求模型、設計模型甚至代碼和代碼的執行模型等.形式驗證是證明不同形式規約之間的邏輯關系,這些邏輯關系反映了在軟件開發不同階段軟件制品之間的需要滿足的各類正確性需求.例如,形式驗證給出“系統設計模型滿足若干特定性質”的證明構造.在形式規約和驗證的基礎上,形式化開發主要是構造、證明形式規約之間的等價轉換和精化關系,以系統的形式模型為指導,逐步精化,開發出滿足需要的系統,也稱為構造即正確(correct by construction)的開發.

形式化方法與其他軟件開發方法[4]的主要區別在于:其描述軟件及其性質的語言是無歧義的,構造和驗證軟件的方法是嚴格的.在軟件工程中,形式化方法提供了工程化系統設計的一種比較透徹的思維方式,可以很好地支持抽象模型建立、系統精化、模型和證明重用;形式化開發過程具有很好的可重復性,相應的軟件制品模型也具有較強的可分析性和可驗證性.因而,形式化方法可以有效地提高和保障系統的可信性.

形式化方法與計算機科學理論密切相關,其發展與程序設計語言和程序理論的發展息息相連.作為一個學科方向,它研究形式化方法的數學基礎、形式系統的表達能力、形式系統的推理系統及其可靠性和完備性,以及在計算系統開發和生命周期各個階段的理論、方法、技術、工具和應用方式等.

1.1 歷史回顧

形式化方法的發展已有較長的歷史,人們主要從兩個角度出發推動形式化方法的提出和早期發展,即,為程序設計提供數學基礎的理論研究角度以及為軟件開發提供嚴格質量保證的軟件工程角度.早在1949年,Turing的論文“Checking a large routine”即討論了程序的正確性問題[5].1962年,McCarthy在IFIP上做了題為“通往計算的數學科學”的演講[6],系統論述了程序語言的形式語義和程序設計理論重要性,直接觸發了形式語義研究.1968年在德國Garmisch召開的NATO軟件工程會議,從提高軟件質量和生產率的軟件工程角度出發,提出了要建立軟件開發和生產的數學基礎;進一步地,軟件的正確性問題和概念成為1969年NATO軟件工程會議的主題之一.形式化方法在這種歷史背景下成為程序設計和軟件工程基礎的重要組成部分,先后出現了一批有重要影響的工作.表1給出了部分圖靈獎獲獎者在形式化方法方面的研究工作.

Table 1 Examples of formal methods researches by Turing Award Laureates表1 部分圖靈獎獲得者在形式化方法方面的研究

1.1.1 圍繞形式語言和形式語義學的基礎研究(1930年～至今)

形式語言是由符號化字母表以及遞歸的語法規則完全定義和生成所有表達式或語句的語言.形式邏輯的語言都是形式語言,如命題邏輯、謂詞邏輯和布爾代數.20世紀30年代,Church用形式語言定義研究計算和算法,提出了一種計算模型Lambda演算[7,8],后來成為函數式程序設計語言、類型論和操作語義的理論基礎.事實上,Lambda演算本身可以看作是一種程序語言.在20世紀50年代末,高級程序設計語言的定義開始了關于計算的形式系統的研究,產生了Backus-Naur Forms(BNF范式)并用于定義ALGOL60,形成了語言的遞歸抽象.形式語言不僅在語言的定義中得到了應用,在系統軟件開發中也發揮了作用,例如,UNIX中的yacc和grep的開發[9].在形式語言定義的同時,如何定義程序的含義成為關注的焦點[10],形式語義學的研究逐漸形成了四大體系:操作語義、指稱語義、代數語義和公理語義.在定義 ALGOL68的語義時,首次使用了“操作語義”這個術語,而McCarthy已在1960年用Lambda演算定義了LISP的語義[11].形式語言理論和形式語義學為形式化方法奠定了基礎,不僅用來定義程序設計語言,形式系統還用來嚴格定義規約語言的基礎,建立了形式規約語言或形式化建模語言.20世紀60年代,Petri提出了Petri Net作為分布式系統的數學化建模語言[12].面向并發系統,Hoare提出了通信順序進程CSP[13,14],Milner提出了通信系統演算CCS[15,16],Hennessy和Lin提出了消息傳送進程的符號互模擬理論[17].隨著軟件形態的不斷變化,形式化建模語言也不斷發展.例如,針對反應式系統,Pnueli在 1977年引入了線性時序邏輯LTL[18],Clarke和Emerson在1981年建立了計算樹邏輯CTL[19];在反應式系統描述的基礎上,發展了面向實時系統的 TPTL[20]、Timed Automata[21]、Timed Regular Expressions[22]和 Timed CSP[23]以及Timed CCS[24],還出現了硬件描述語言、體系結構描述語言、通信控制建模仿真語言等.

1.1.2 圍繞形式規約和開發的方法學研究(1970年～至今)

直接使用程序設計語言及其語義難以描述和證明軟件從需求文檔到程序代碼的開發過程各階段創建的不同抽象層次的制品及其正確性,人們開始研究高層抽象的形式規約語言的設計,形成了以形式規約語言為基礎的形式化開發方法.例如 VDM[25-27]、Z[28]、Event-B[29]、RAISE[30,31]、CafeOBJ[32]、TLA+[33]、rCOS[34]、SOFL[35]等等.形式化開發利用形式規約語言對軟件建模并描述其所期望的軟件性質,提供指導開發人員進行精化的方法,進行形式規約之間(部分的)一致性檢查和證明.基于不同的開發方法,形式規約可以自頂向下逐步精化形成開發的規約序列,在足夠的實現細節完成后,可以通過代碼自動生成得到程序.例如,VDM 的精化有數據具體化(data reification)和操作分解(operation decomposition)等.形式化方法逐步建立了工具集,以支持形式規約的性質分析和證明,例如Z/EVES[36]、Event-B/Rodin[37].1970年代后,軟件工程界認識到了數學可以為保證程序正確性提供技術基礎,形式化方法(formal methods)一詞開始傳播開來.1980代初,唐稚松提出以時序邏輯作為軟件開發過程的統一基礎,并著手建立XYZ系統[38].在1980年代到90年代,形式化方法得到了重視,特別是歐盟大力支持了形式化開發方法的研究.例如Concur、ProCoS、REACT等.人們希望能夠利用形式化方法高效、高質量地開發軟件,這一方面有力地促進了形式化方法和技術的發展;另一方面,由于應用規模較小,效果證據不足,應用方式不明確,工業界對形式化方法的看法出現了爭議.在形式規約和開發的方法學基礎方面,Goguen和 Burstall提出了機構(institution)的抽象模型理論,用以建立語言語法驅動的、不同形式邏輯基礎上的各種形式化方法的理論統一以及技術和工具集成與和諧使用[39];Hoare和何積豐提出了統一程序設計理論框架 UTP,提供了在一種程序(如順序程序)語義模型理論基礎上構建擴展程序(如并發)的語義理論,從而保證原來的理論在擴展的理論中重用,并同時建立了操作語義、指稱語義、公理語義和代數語義的互聯統一[40].

1.1.3 圍繞形式驗證技術的工程化研究(1980年～至今)

建立了形式規約之后,如何從形式規約開發得到正確的系統成為關鍵.形式驗證,包括如何證明不同抽象層次的規約間等價或者滿足精化關系、如何驗證形式規約(所要求的性質)及其模型之間的滿足關系,是形式化方法保證軟件開發正確性必須解決的科學問題和實際應用問題.形式驗證理論涉及了數理邏輯的傳統基礎問題.在研究驗證自動化過程中,發現了相關大量的不可判定問題、NP完全問題以及狀態爆炸等否定性的結果.否定性的結果同時推動了各種可組合的規約證明技術、抽象解釋技術以及提高實現效率的數據結構(如BDD).這些研究同時促進了形式化技術與傳統測試和仿真技術的結合,形成了新的基于形式化的測試和仿真技術.這些技術將重點放在軟件的缺陷檢驗和調試上,以發現錯誤為首要目的[3],出現了形式驗證及其工程化技術和工具,包括以 SAT/SMT為代表的約束求解、基于交互式輔助定理證明工具的機械化驗證、以模型檢驗為代表的自動分析與驗證.工具的自動化水平和可擴展能力得到了顯著的提高,如SAT/SMT求解器Chaff[41]、Z3[42]、CVC4[43],定理證明環境 ACL2[44]、Isabelle/HOL[45]、Coq[46]和 PVS[47],模型檢驗工具 SMV[48]、SPIN[49]、UPPAAL[50],PRISM[51]、PAT[52]等等.形式驗證在硬件驗證中獲得了巨大的成功,也不斷地進入嵌入式軟件、安全攸關軟件等高安全等級軟件的開發.Pnueli在他的圖靈獎演說中稱,驗證工程(verification engineering)是未來的職業[53].

1.1.4 以可驗證軟件為目標的多學科交叉研究(2000年～至今)

1999年,在關于計算機科學技術面臨的巨大挑戰的討論中,Hoare提出了驗證編譯器(verifying compiler)倡議(后稱為verified software).經過幾年的調研和準備,2005年召開了第1屆VSTTE(verified software:Theories,tools,experiments)會議.來自世界各地的專家討論了形式規約、構建和驗證高質量軟件的方法,形成了可驗證軟件計劃,希望[54]:(1) 建立能夠構建實際可靠的程序的設計理論;(2) 建立一組支持上述理論的自動化工具集,并且能擴展至具有工業化能力;(3) 建立已驗證的程序庫,能夠在實際系統中替代未驗證的程序,并能以可驗證的狀態持續演化.2007年,我國國家自然科學基金委也開展了“可信軟件基礎研究”重大研究計劃[55-57],形式化方法作為其中的重要途徑來提高軟件的可信性.經過 10余年的努力,形式化方法進入了硬件設計的標準流程,也出現了驗證過的編譯器[58]和微內核操作系統[59].人們普遍認可了形式化方法對于深刻認識計算系統和提高軟件質量的貢獻.美國NITRD在計算使能的網絡化物理系統(CNPS)、網絡空間安全和隱私(CSP)、軟件生產力、可持續和質量(SPSQ)等多個領域(PCA)突出了形式化方法的位置,NSF連續資助了形式化方法領域的大規模探索項目 CMACS[60]、EXCAPE[61]、DeepSpec[62]等.DARPA的項目 HACMS[63]利用形式化方法成功地研發了可以免于黑客攻擊的無人機操作系統和飛行控制軟件.形式化方法在計算機軟/硬件開發和質量保證上發揮了重要作用,與人工智能相結合的程序綜合、大數據以及與形式推理相結合的軟件自動化重回熱點前沿.此外,形式化方法在網絡安全、量子計算、生物計算等方向的交叉應用也受到了廣泛關注.

1.2 形式化方法的基本體系

圖1給出了基于形式化方法進行軟件開發的基本框架.與基于模型的軟件開發類似,通過需求分析得到初始形式規約Spec1;然后,經過逐步求精或者轉換,得到一系列精化后的形式規約(Spec2,…,Specn);最后,可轉換或綜合生成得到系統的程序代碼實現.Spec1,...,Specn都是對系統的抽象(建模),它們的抽象角度和層次不同.

Fig.1 Framework of formal (development) methods圖1 形式化方法軟件開發框架整體圖

圖1中還給出了形式規約語法、語義以及形式規約之間的關系.給定形式規約Speci,由語義函數[[_]]給出其在數學域上的形式語義[[Speci]](即Semanticsi).規約之間的邏輯關系(如精化關系可以描述為邏輯中的蘊含“→”)與相應數學理論(如集合論中的集合包含“?”)有對應關系(如,若Spec2→Spec1,則[[Spec1]]?[[(Spec2)]]).在軟件開發中,規約不必僅用同一種形式語言描述,不同的規約語言之間的關系可以基于某個統一的形式理論,例如Institutions[39].

綜上所述,形式化方法是由形式規約語言(包括形式語義與模型理論)、形式規約(包括精化與綜合)、形式驗證、形式化工具等形成的一個整體.其中,形式規約語言是基礎,形式化方法中,軟件制品是規約語言編寫/變換的形式規約;形式驗證是保證開發正確性的途徑,形式語義與模型理論是聯接形式規約和形式驗證的數學紐帶;形式化工具是系統設計和開發中高效使用形式化方法的需要和實踐.

2 形式規約

形式規約是由形式規約語言嚴格描述的系統模型或者系統需要滿足的性質.前者是模型規約,后者是性質規約.形式規約是形式化方法的基礎[64].在軟件分析[2,3]中,動態執行測試或驗證技術以及動態在線跟蹤監控和驗證也經常使用形式規約.

本節我們討論形式規約語言及其語義的定義方法、形式規約和語義模型之間的關系,并在此基礎上介紹形式規約在軟件構造中的應用.

2.1 形式規約語言

形式規約語言是指由嚴格的遞歸語法規則所定義的語言,滿足語法規則的句子稱為合式或良定義規約(well-formed specification).

2.1.1 模型規約語言

模型規約語言利用數學結構描述系統的狀態變化或者事件軌跡,它直接定義所描述系統模型的結構、功能行為甚至非功能行為(如時間).模型規約給出了系統開發過程中不同抽象層次的模型,有相應的邏輯推理系統支持其分解和組合,完成不同層次間規約的轉換和精化.主要包括如下幾類.

(1) 代數規約語言

一個代數規約由一些表述類子(sort)的符號、類子之間的運算符(operation symbol)以及在多類等式邏輯(many-sorted equality logic)中的等式公理組成.代數規約的一個模型就是滿足該規約的異構代數.為了語義的唯一性,一般采取初始代數(initial algebra)為規約的語義.代數規約的優點是具有非常好的數學基礎,任意操作序列的計算結果可以自動得到、自動執行,例如4GL(fourth generation programming languages).等式邏輯的表述能力有較大局限性,不能表達一般的程序結構和行為.因此,后來代數描述中引進了帶歸納的一階邏輯,同時引進了支持偏函數和子類,模塊化結構和模塊組合的架構機制,形成了一個通用代數規約語言(the common algebraic specification language,簡稱CASL)[65].其他的代數規約語言還有OBJ[66]、PLUSS[67]、Larch[68]等.代數規約對程序設計理論和軟件工程影響非常廣泛,例如早期的抽象數據類型[69],后來的面向對象程序設計[70,71]、ML等函數式程序設計語言[72],等等.

(2) 結構化規約語言

早期的結構化模型規約語言有VDM-SL[27]、Z Notation[28,73]等.VDM包括數據類型的規約和程序結構(即模塊)的規約.數據類型的規約定義具有該類型的數據以及數據上的操作,由一階謂詞邏輯描述數據的范圍約束以及操作需要滿足的約束.一個模塊的規約說明程序變量及其類型以及一組過程或函數.過程和函數的功能約束由Floyd-Hoare邏輯來定義.VDM定義了模塊的組合機制.Z-語言的Z-模式(Z-schema)可以描述數據類型和程序功能,并統一使用一階謂詞邏輯描述集合、函數和關系,故而其邏輯基礎是一階謂詞邏輯和集合論.Z-語言的模塊組合機制與VDM相似.VDM和Z都是以精化為核心的規約語言,支持軟件從需求規約到代碼規約的自頂向下的瀑布開發過程模型.由于一階邏輯包含在規約語言中,所以可以描述模型規約需滿足的性質.如果規約蘊含該性質,則該歸約滿足此性質.因此,VDM和Z也支持包含分析驗證的V型開發過程模型.

為了提供面向對象的軟件規約和精化,VDM擴展到VDM++[74],Z擴展為Object-Z[75].在VDM和Z的基礎和思想的影響下,為了處理交互的分布式軟件和基于服務的系統,在類似基于數據狀態的VDM和Z的靜態規約語言中引進了事件和狀態遷移行為,發展了一系列的規約語言,包括 B[76]、Event-B[29]、Alloy[77]、JML[78]和rCOS[34]等,這些規約語言都有明顯的軟件結構描述,其中,JML和rCOS直接使用了現代高級程序語言的結構機制表示軟件架構,例如面向對象的繼承和基于構件的軟件界面和連接器(connector).

(3) 進程代數(演算)

為了設計開發并發和分布式系統,出現了CCS[15]、CSP[13]、ACP[79]等進程代數(演算).CCS和CSP都最大限度地將并發通信系統的數據狀態和數據計算功能抽象掉,集中描述通信和同步以及二者之間的關系,是基于事件的規約語言.CCS規約是一個CCS語法定義的表達式,語義是通過結構操作語義來定義表達式描述的通信進程的行為演化.這樣定義的CCS表達式的狀態遷移規則構成了推導CCS表達式之間各種等價關系的形式系統,這些等價關系可以表示成不同的互模擬(bisimulation)關系.CSP有比較豐富的程序語言因素,例如外界選擇、內部選擇、同步并發等.CSP定義了一系列不同抽象層次的指稱語義,按表達能力遞增的順序有軌跡語義(trace semantics)、失效語義(failure semantics)和失效-發散語義(failure-divergence semantics).后來,CSP也有了完整的操作語義理論.基于進程代數的規約具有非常好的結構特征,適合對復雜系統,特別是并發、并行和分布式系統進行建模.

為了處理并發系統的其他特征,如信息安全、移動、實時、混成、概率和隨機,這些并發模型均進行了各種擴充.例如,為了處理實時系統,Reed和Roscoe擴充CSP到實時系統,建立了Timed CSP[23];為了處理混成系統,何積豐和周巢塵等人將 CSP擴充到混成系統,建立了混成 CSP[80-82].再如:為了處理移動計算,Milner提出了π-演算[83],后被Cardelli和Gordon進一步擴充為Ambient-calculus[84];為了處理信息安全,Abadi等人將π-演算改進成spi-演算[85];等等.Milner試圖使用范疇論統一這些并發計算模型,提出了Bigraph理論[86].

(4) 基于遷移系統的規約

遷移系統可以自然地表示系統的行為.典型的基于遷移系統的規約語言有Petri網[12]和Statecharts[87]等.基于遷移系統的規約語言往往有圖形化表示,稱為可視化規約語言.Statecharts用Higragh進行形式定義,圖的節點代表系統執行的狀態,而一個節點到另一個節點的邊表示從一個狀態到另一個狀態的遷移,可將模型轉化為規則形式定義,構成一個推理系統.由于其執行模型是抽象機,這樣的圖形語言可以構建可執行的規約(executable specification)或可執行的模型(executable model),能夠對系統行為進行仿真、測試.它們經常作為時序邏輯的解釋(模型)使用,可以用時序邏輯進行規約和證明其性質,也可用算法判定其建立的模型是否滿足一個時序邏輯公式.結果可以作為系統早期設計驗證的依據,以便盡早發現設計錯誤.但是這種形式規約組合性較差,不容易對復雜系統建模.

為了對非功能性需求建模,人們對標記遷移系統進行了各種擴充.以自動機為例,其后續擴展包括:時間自動機[21]、混成自動機[88]、概率時間自動機[89]、隨機混成自動機[90],等等.而且這些模型不再局限于計算機領域,已經廣泛應用于控制、生物、物理、化學等諸多領域.

2.1.2 性質規約語言

性質規約語言基于程序邏輯系統,通過邏輯公式來描述一組性質以定義所期望的系統行為.性質規約不直接定義系統的具體行為.基于性質的形式規約偏向于說明性的,邏輯約束往往是最小必要的,以給出較大的實現空間.Lamport指出,系統需要滿足的性質可以分成兩類[91]:安全性質,即不好的事情從不發生;活性,即好的事情一定能夠發生.Alpern和Schneider證明,任何性質均可以表示成這兩種性質的交[92].

順序程序設計早期的程序邏輯是Floyd-Hoare邏輯[10,93].Floyd-Hoare邏輯的公式形如{Pre} P {Post},其中,Pre和Post是一階邏輯公式,分別稱為前、后置斷言;P是程序.通常,{Pre} P {Post}可以有如下兩種解釋.

a)部分正確性:如果一個初始狀態滿足 Pre,且P由該初始狀態的執行能夠終止,那么終止狀態一定能夠滿足Post;

b)完全正確性:如果一個初始狀態滿足 Pre,那么 P由該初始狀態的執行一定能夠終止,且終止狀態一定能夠滿足Post.

Floyd-Hoare邏輯的推理系統是在一階謂詞系統基礎上添加關于程序的公理和推理規則來建立的.類似的規約語言有Dijkstra的衛士命令語言的最弱前置條件演算[94].

然而,這些早期的奠基性工作有很多不足之處,如缺少對帶指針和內存數據結構的程序規約機制、缺少并發程序的規約機制等等.后期有大量工作對Floyd-Hoare邏輯進行擴展,形成了新的程序邏輯、規約和驗證方法.分離邏輯[95]是對 Floyd-Hoare邏輯的擴展,以支持帶有指針和內存數據結構的程序的驗證.它由 Reynolds、O’Hearn、Ishtiaq和Yang等人在2000年前后提出,是近年來程序規約與驗證領域的最重大突破之一.它在斷言語言中引入方便描述內存形狀和分離特性的分離合取和分離蘊含謂詞,并在規則中將Floyd-Hoare邏輯的不變式(invariance)規則替換為框架(frame)規則.分離邏輯最大的特色是對內存和數據結構的抽象描述,它能夠更方便、更模塊化地支持類似C程序的指針程序的驗證.

在 Floyd-Hoare邏輯的基礎上,通過引入行為軌跡的變量或不變式,建立了多個并發程序的規約語言,有代表性的工作主要包括 Owicki-Gries方法[96,97]、Rely-Guarantee方法[98,99]和并發分離邏輯[100].與分離邏輯類似,并發分離邏輯對并發程序驗證有很好的模塊化支持.在其被提出之后,有大量工作對并發分離邏輯進行擴充,包括將 Rely-Guarantee和并發分離邏輯結合,以支持細粒度并發或者無鎖并發程序的規約和驗證.基于并發分離邏輯開展的工作可參見 Brookes和 O’Hearn的綜述文章[101].除了這些針對串行一致性內存模型上的并發程序的程序邏輯外,近年來還有一些工作對并發分離邏輯進行擴展,以支持弱內存模型下的并發程序.比較有代表性的工作包括Vafeiadis及其團隊提出的一系列在C11內存模型上的程序邏輯(如文獻[102]),以證明C11內存模型(子集)上的程序的正確性.

為了克服Floyd-Hoare邏輯中程序和斷言的分離及無法表達活性,Pratt提出在模態邏輯中使用程序來定義模態算子,建立動態邏輯[103].Kozen在動態邏輯中引入不動點,建立模態μ-演算[104].在樹結構上,它的表達能力和二階一元邏輯等價[105,106].線性時序邏輯(LTL)[18,107]和計算樹邏輯(CTL)[108,109]是并發系統規約和驗證的常用語言.LTL和 CTL的表達能力不可比較,但都是模態μ-演算的真子集;Lamport提出了動作時序邏輯(TLA)[110];Moszkowski等人提出了區間時序邏輯(ITL)[111].為了處理一些非功能性質,這些邏輯均作了一些擴充.例如,動態邏輯被擴充到混成系統,稱為微分動態邏輯[112];LTL擴充到實時系統,稱為度量時序邏輯(MTL)[113];LTL和CTL分別擴充到概率系統,稱為pLTL[114]和pCTL[115];ITL擴充到實時系統,稱為時段演算(DC)[116,117]等等.

2.2 形式語義學

形式語義學起源于對程序設計語言語義的研究.程序設計語言的語法是符號化的,其語義就是該語言程序所描述的計算或者過程.在程序設計語言的早期,語義用自然語言解釋,程序語言的解釋器或編譯器按照語義將該語言程序編譯成計算機可處理的機器語言程序.這種自然語言解釋的語義不精確、有歧義,無法支持對程序正確性的嚴格證明和分析.為了幫助理解使用程序設計語言、支持語言標準化、指導語言設計、幫助開發更好的編譯器以及分析證明程序的性質和程序之間的等價性,需要對程序語言的語義進行抽象和嚴密的定義.為此,出現了使用數學結構來定義程序語言語義的研究,后擴展到各類形式規約語言,形成了形式語義學.形式語義學(理論)研究形式規約語言語義的數學基礎和構建方法,提供研究形式語言表達能力、可靠性和完備性的數學手段.依據使用的數學結構和語義表示方法的不同,形式語義研究方法可以分為 4類,即操作語義、指稱語義、代數語義和公理語義.關于計算機語言的形式語義的綜合論著可參閱文獻[118,119].

2.2.1 操作語義

操作語義(operational semantics)使用抽象解釋器(有時也稱為抽象機或者抽象函數)定義語言語義,著重模擬數據加工過程中計算機系統的操作.定義操作語義需要一個抽象機模型.最早有形式語義的語言是 McCarthy用Lambda-演算定義的LISP,Lambda-演算的表達式求值過程是用抽象機定義的.1981年,Plotkin提出了結構化操作語義[120]作為定義程序設計語言的方法.目前最為常見的是標號遷移系統(labeled transition system),基本想法是把程序執行描述成標號遷移系統,其中的狀態為程序執行期間任意時刻觀察到的變量取值,遷移關系規定如何從一個狀態遷移到下一個狀態,一般定義為一組遷移規則,每條遷移規則對應一個語句,稱為標號.一條語句的語義是由一組以其為標號的規則定義;標號規則具有組合性,即,一個復合語句的規則可以由其成分語句的規則組合而成.

操作語義是最早使用的形式語義方法,用來給出順序程序的語義,此時,狀態均是一些簡單的數據結構,遷移關系一般都是確定的、離散的,也不需要考慮標號間的通信和同步.為了定義復雜程序的操作語義,例如面向對象程序、并發程序、實時程序、概率程序、混成系統等,人們對遷移系統進行了各種擴充,或擴充它的狀態,或擴充它的遷移關系,亦或兩者同時擴充.例如,為了定義面向對象程序,人們擴充了程序狀態,引入堆和棧等復雜數據結構[121];為了處理并發程序,人們擴充了標號遷移關系,允許使用標號描述通信和同步[83];為了描述概率和隨機程序,允許以給定的概率或者隨機選取遷移規則[122]等等.

操作語義基于抽象機,與計算機最為接近,可描述實現方面的執行細節,操作性比較強,適合于開發語言編譯器以及編譯優化的應用.在語義中,狀態是被直接表示和操作的,也比較適用于形式驗證中基于狀態搜索的模型檢驗方法里的語義模型.然而,在大規?；驘o窮狀態的系統中,抽象機上的推理系統比較弱,不易進行基于演繹推理的形式驗證.

2.2.2 指稱語義

指稱語義(denotational semantics)將語言的基本語法成分解釋成為數學對象(稱為指稱),用數學對象上的運算來定義語言的語義.論域理論是指稱語義的數學基礎,討論各種語言成分的指稱的數學結構,并提供數學工具,從而在各種數學結構之上定義語言語義和推導語言成分特性.例如,將程序語言的基本語法實體的指稱定義為程序狀態空間上的函數和泛函,復合語法實體的指稱由構成它的子成分的指稱復合得到.

建立指稱語義的首要任務是確定一個相應的論域理論,即確定程序語言的解釋域[123].處理不同的計算現象需要不同的語義,例如,可以定義不關心是否停機的順序程序的語義,也可以定義需要刻畫停機的語義.顯然,不同的語義需要不同的論域.以CSP為例,Hoare等人提出了CSP的跡語義模型、失效-發散-跡語義模型等[14,124],這些語義的區別在于失效-發散的語義可以刻畫程序死鎖以及活鎖,從而分析系統的活性.論域理論的研究隨著程序對象的不同而不斷地發展著,例如,針對 Timed CSP,人們擴充了跡語義模型和失效-發散-跡語義模型,分別提出了帶時間戳的跡語義模型和帶時間戳的失效-發散-跡語義模型[23,125].

指稱語義的論域理論具有較多可利用的數學性質,有利于探討不同語義論域及不同語義間的關系,特別是與公理語義和操作語義間的關系.論域表示理論討論了不同語義論域間的關系,提供了不同語言形式語義間的關系[126];Hoare和何積豐基于一階關系演算提出了程序統一理論(unifying theories of programming,簡稱UTP)[39],其基本想法是,通過伽羅瓦連接(Galois connection)給出同一語言不同語義間的轉換關系.指稱語義可以較好地支持形式規約的精化.

2.2.3 代數語義

代數語義(algebraic semantics)用代數結構來定義計算機語言(特別是代數規約語言)的語義,是在抽象數據類型的基礎上發展起來的[118].在抽象數據類型中,基調是用代數結構描述數據類型的語法(類子和類子間的運算),運算的推導規則用一組公理(等式或者條件等式)描述,這樣,滿足這組公理的模型就是這個抽象數據類型的一個代數語義(稱為∑-代數,其中,∑是基調).基于代數語義,可以利用模型論和范疇論方法來推理該語言的程序性質.

抽象數據類型將數據對象及對象上的操作封裝、數據類型的特性與實現分離,具有模塊化和可復用的性質.它與軟件開發過程匹配比較自然,首先設計較小的抽象數據類型,然后逐步擴充形成較大的抽象數據類型體系;這個過程中,抽象數據類型間可討論層次一致和充分完備等性質.一個抽象數據類型可能有多個語義模型,其中,初始代數(initial algebra)和終結代數(terminal algebra)在∑-同構意義下都分別唯一,采用初始(終結)代數模型作為語義的方法稱為初始(終結)語義方法.抽象數據類型基始完備的描述可以唯一地擴充為相對完備,原描述的終結模型恰好就是其極大擴充的初始模型,表明了初始代數語義與終結代數語義之間的內在聯系[127].把一個規約或程序視為抽象數據類型時,就有了它的代數語義.對于規約或程序,可能對某些輸入是無定義的,故定義了偏抽象數據類型和偏∑-代數.另外,在處理程序開發中,兩個不同的程序會有相同的執行效果,相應的代數語義要處理好等價的問題.

代數語義與代數規約的關系密切,主要用于解決基于代數規約的形式化開發中程序正確性的推理,抽象程度比較高.如果將等式看作是從左至右的重寫規則,代數規約就以項重寫的形式可執行,成為了一種可執行規約.

2.2.4 公理語義

公理語義(axiomatic semantics)直接使用形式邏輯來描述程序的語義,其基本思路是,在已有的形式邏輯系統的基礎上增加所有程序必須滿足的基本命題(程序公理).每個程序的基本語句都有一組公理和推理規則,它們與斷言邏輯一起構成程序邏輯的證明系統.程序性質的規約和驗證就可直接在該形式系統中進行.程序邏輯的表達能力、可靠性、完備性以及可判定性都可歸結為數理邏輯上的元性質,程序邏輯的解釋模型通常就是程序語言的指稱語義或操作語義.

最為常見的有基于一階邏輯擴展的Floyd-Hoare邏輯、謂詞轉換器(predicate tranformer)等.Floyd-Hoare邏輯最初是針對順序程序提出來的,并擴展至并發程序、實時系統、混成系統甚至量子系統等.面向指針程序和面向對象程序產生了分離邏輯及其變種,這些研究把 Floyd-Hoare邏輯的應用真正地推進到實際的程序驗證.人們還提出了動態邏輯、模態邏輯、時序邏輯等用來作為定義程序公理語義的形式系統.公理語義在形式驗證中的應用是比較多的.

表2給出了這4種語義之間的一個比較.程序語言的形式語義的機器定義是建立形式驗證的基礎.例如,可以使用定理證明器的元語言來機器實現程序語言的語義,也可直接用函數式語言來實現目標程序語言的語義.K框架基于重寫的可執行語義框架,用來定義程序語言的操作語義,能夠解釋執行程序、空間搜索和模型檢驗,支持該語言程序的驗證[128].基于K框架,定義了C99和Java 1.4的形式語義[128,129].

Table 2 Comparsion of formal semantics表2 形式語義風格之間的比較

2.3 形式化開發與軟件構造

形式規約和開發方法遵循軟件開發方法的基本原理,包括關注點分離和逐步精化.在形式規約和驗證的基礎上,軟件形式化構造活動包括針對形式規約多視角建模、不同抽象層上規約間的精化以及程序綜合等.

2.3.1 基于規約的形式化開發

形式規約必須具有良好的性質.形式系統的一致性表明其是否語義可滿足,換言之,形式規約的一致性刻畫了其是否是可實現的.即:它對應滿足關系的語義域非空,說明這個規約有滿足其約束的實現,理論上是可實現的.當形式規約用來描述需求時,則成為判斷需求規約可行性的重要途徑.另一方面,一般不要求形式規約是完備的,不完備的規約可以給實現者更多實現方法上的空間,也給了開發人員平衡未來實現在功能和性能上的空間.一個規約本身就可以有多個不同的實現,例如實現的數據結構和算法.

與軟件的其他建模方法一樣,形式規約可以從不同的角度用不同/相同的規約語言來描述系統,即所謂的多維視角規約方式,如圖2所示.例如,一個系統(需求)規約可包括數據模型規約、數據功能規約、交互通信協議規約以及動態的狀態遷移行為模型.復雜的系統還會有更多的視角,尤其是非功能方面的.數據模型可以用代數規約或Z-語言[73]描述,數據功能規約可以用Floyd-Hoare邏輯[93],交互通信協議可以用CCS[15]、CSP[14]等,而動態行為可以用自動機[130]或 Statecharts[87].功能規約描述系統功能和子功能之間的關系,例如數據功能規約和交互模型.行為規約描述系統的時序、容錯、時空等約束.系統規約往往是相互關聯的,各個視角規約內部和規約之間都有一致性約束,以保證規約是可實現的,而系統同時滿足這些約束就能得到系統完整的正確性.多視角的形式規約有模型的,也有性質的,或者兩者混合的.使用不同語言需要各種語言語法和語義的一致統一,對此,rCOS在UTP基礎上有初步的研究結果[131].也可以用單一的形式規約語言,如Event-B[29].但是每種語言一般都有局限性,理論和工具支持也不夠充分,所以有必要進一步推進各種形式化方法在 Institutions[39]或者 UTP[40]等的基礎上的統一及工具的集成.

環境建模是軟件開發中不可忽略的內容,形式規約同樣需要包括對環境模型或性質約束的規約.在包含了環境的形式規約中,要區分環境與系統建模的不同,環境規約是一組假設[64].例如在模型規約中,環境狀態和變遷在可觀、可控上的不同.對于大型復雜系統的規約,我們需要盡可能顯式地表達出對環境的假設,同時選擇合適的部分規約的抽象層次和形式,以靈活應對環境的動態和多變.含環境的規約一般可以定義為系統或構件的接口合約(interface contract).合約的抽象形式是一組關于系統和環境的謂詞(A,G),其中,A描述系統環境應該滿足的條件,G是在環境滿足A的前提下系統行為所滿足的要求.

Fig.2 Formal development methods—Multiple views圖2 形式化開發方法——多維視圖

軟件開發過程中,形式規約方法與設計方法一樣是逐步開發的.以形式規約為制品的設計形成了形式化開發的主線.形式化開發中最重要的設計活動是精化,它是將形式規約的抽象層次向實現加以變換.例如,一個層次的模塊分解為下一個層次的若干模塊,或者具體化一個抽象數據類型的表示類型.精化需要保持正確性,并具有組合性,不同抽象層次逐步開發的形式規約形成了規約的精化鏈.基于合約的規約有很好的可組合性并支持建立精化演算.圖2所示的需求分析結果可以是系統或構件與環境的合約規約,而架構設計中子系統或構件C1和C2在各自的合約基礎上加以組合,計算出組合系統的合約規約,并保證是上層合約的精化,即保證滿足上層規約的所有需求性質.整個設計過程可以理解為一個逐步分解和精化的過程.

精化演算是以組合化方式支持逐步求精的形式推理系統,最早是面向順序程序[132,133],近年來發展到了反應式系統精化[134,135]和構件化軟件的精化[34].在形式化逐步求精過程中,精化都可以是形式化的,每步精化需要證明下一層的規約滿足上一層的規約,.在實際應用中,因為成本問題,工業界往往不這么做.但是,有精化演算指導的設計過程無疑能提高設計質量.軟件工程中建立的一系列設計模式(design pattern)在一定意義上就是對精化技術的一種非形式化的工程實踐.如果在安全攸關的應用開發時能夠盡可能地形式化,則對于確保安全性是有顯著意義的.在形式化開發中,精化過程的一種重要技術是程序綜合,即,從規約能夠直接生成程序,參見第2.3.2節.

在逐步求精的過程中,形式化方法有效支持關注點分離的軟件工程原則.一般情況下,數據功能、交互通信協議和動態規約可以分別求精;從無時間的規約到有時間的規約一般可以是精化(時間模型的健康條件)[40],容錯也可以視為原來設計規約的精化[136].另外,基于形式化的設計精化一般有很好的可組合性,分解和精化支持模型重用、證明分析過程重用、代碼重用,所以有效支持分而治之的工程原則,尤其是基于構件和服務化系統的開發.

研究、理解和處理軟件開發的復雜性,一直是驅動軟件工程發展的核心問題.針對Brooks指出的軟件開發復雜性來源[137],形式化開發從需求規約到軟件代碼,將軟件開發建立在一個有理論基礎和規則的工程過程中,這正是1968年NATO軟件工程會議所提出的目標.我們可以使用形式化方法討論和說明一種軟件開發方法的科學性以及開發過程的可信性.在這個過程中,形式化可以提高開發的嚴密性,用抽象和分解手段有效處理復雜性,尤其是通過精確描述復雜系統行為、基于精化的設計、將開發過程制品轉換成可以分析驗證的規約等手段,能夠有效地提高在巨大的設計空間中逼近最合適設計的能力.

2.3.2 程序綜合

程序綜合(program synthesis)是指使用指定的編程語言自動生成符合程序規約的技術.程序綜合問題由Church[138]于1960年代初提出,一直是計算機科學的核心問題和挑戰,被認為是計算機科學的圣杯[139].最初關于程序綜合的方法是基于轉換的程序綜合(transformation-based synthesis)[140],它將一個高層的程序規約通過反復轉換為較低層的程序規約,最終生成期望得到的程序代碼.規約間或規約與程序間的轉換要么歸結為樹自動機接受語言是否為空的問題[130],要么歸結為兩個玩家博弈取勝的策略問題[141].但這種方法能夠自動生成的代碼非常有限,很長一段時間沒有發展.近些年,隨著Pnueli提出由時序邏輯公式自動綜合反應式系統控制程序的成功,有復蘇跡象[139].

現在較為流行的程序綜合的方法主要基于演繹推理的方法及其變種,特別是與人工智能相結合的方法.在構造數學中,1930年代即有了通過把子問題的解組合到一起的方式來構建證明的思想[142].在第一個自動定理證明器開發出來之后,人們提出了許多基于演繹推理的演繹綜合(deductive synthesis)方法[143-145],主要思想是:首先,使用定理證明器構造用戶提供的程序規約的一個證明;然后,基于Curry-Howard同構關系[146],使用該證明來生成相應的程序代碼.

基于演繹的綜合方法假定用戶可以提供需求的一個完整的形式規約.但在很多情況下,提供一個完整的形式規約并不比寫出一段程序更加容易.為此,人們提出歸納式程序綜合(inductive program synthesis).歸納式程序綜合基于歸納式規約,例如輸入輸出對、示例(demonstration)等.Shaw等人[147]發展了從單個輸入輸出樣例中學習語法受限的LISP程序的框架.Summers[148]和 Biermann[149]發展了一種從多個輸入輸出對中學習語法更加豐富的LISP程序的方法.Smith[150]發展了以一系列程序執行記錄為示例來推斷遞歸程序的方法.除此之外,有很多開創性的工作通過基因編程的技術來自動進化出符合規約的程序[151].這些方法從達爾文的進化論中得到啟發,通過持續不斷地將一個隨機種群進化到新的世代,最終生成所需的代碼.

還有一些方法允許用戶在程序規約以外提供代碼框架(或是語法).這樣做有如下兩個優點:首先,提供的語法極大地縮小了代碼空間,從而極大地提升了搜索效率;其次,由于程序是按照給定的語法生成的,學習到的程序更容易讀懂.SKETCH[152]系統允許用戶提交代碼片段,然后再根據用戶提交的規約補全代碼片段.FlashFill[153,154]使用正則表達式定義了一個操作字符串的領域專用語言,然后基于解釋空間(version-space)的代數來高效地從輸入輸出對中獲取對應的程序,在微軟表格中得到了廣泛的應用.

很多現代程序綜合方法建立在多種生成框架之上.這些框架不僅允許用戶定義程序空間,也允許用戶定義生成程序的一些性質.然后,程序綜合框架將這些定義包裝成一個在給定問題域內的高效的程序生成工具,例如SKETCH[152]、PROSE框架[155]和ROSETTE虛擬機[156].

3 形式驗證

形式化方法最顯著的作用是能夠對形式規約進行驗證.形式驗證常見的有兩種形式:一種是推理“系統模型規約是否滿足其性質規約”,這時,模型規約偏向操作型,性質往往是說明型的;另一種是推理“系統的一個模型規約是否與另一模型規約有精化或等價關系”.這些推理過程給出了一套靜態方法來預測系統的行為:用戶可以描述系統行為的所期望性質或者開發過程中不同抽象之間關系的猜想,形式驗證通過機械化的方式來證實或者證偽這個性質或者猜想,從而提高用戶對規約和系統的可信程度.形式驗證方法主要包括演繹式的定理證明和算法式的模型檢驗.

3.1 定理證明

基于定理證明的形式驗證將“系統滿足其規約”這一論斷作為邏輯命題,通過一組推理規則,以演繹推理的方式對該命題開展證明.基于定理證明的驗證大部分是以程序邏輯為理論基礎的,但是程序邏輯并非唯一的驗證方法,例如,我們可以基于程序的操作語義直接表達程序執行的安全性、正確性等各種性質并證明相關定理[58,157].

Floyd-Hoare邏輯[10,93]是一種經典的基于定理證明的驗證系統,其驗證對象是順序程序.Floyd-Hoare邏輯通過一組和程序語言語句對應的公理和規則,將對程序的驗證轉化為一組數學命題的證明,這組數學命題往往稱為驗證條件(verification condition,簡稱VC).Owicki和Gries提出一種通用的并發程序驗證方法[96],該方法將每個并發任務當作順序程序單獨進行驗證,然后檢查任務之間的無干擾性(non-interference),以確保單個并發任務的驗證過程不會因為其他并發任務的執行而變得無效.這種方法的問題是缺少可組合性,這是由于在進行無干擾性檢查時,需要檢查所有并發任務的代碼,因此并不能在真正意義上實現對單個并發任務進行獨立驗證.Jones在此方法的基礎上進行擴充,提出了Rely-Guarantee方法[98],解決了可組合性問題.Rely-Guarnatee方法將并發任務間的接口抽象為Rely和Guarantee兩種不變式——Guarantee是對任務自身行為的抽象,而Rely則是對任務所能接受的環境行為的抽象.在檢查任務之間的無干擾性時,不需要逐行檢查任務的代碼,只要檢查不同任務之間的Rely和Guarantee接口的匹配即可,要求每個任務的Rely被其他每一個任務的Guarantee蘊含(即Rely得到滿足).由于不再需要逐行檢查所有任務的代碼,Rely-Guarnatee方法允許對單個任務進行獨立驗證,因此是一種具備可組合性的方法.

除了通用的Owicki-Gries方法[96]外,Owicki和Gries還針對良好同步(properly synchronized)的并發程序提出了一種簡化的程序邏輯[97].邏輯要求并發任務對共享數據的訪問必須在互斥鎖所保護的臨界區內進行.共享數據必須滿足一定的不變式,該不變式構成了并發任務之間共享數據的協議.每個任務進入和退出臨界區時,必須保證共享數據滿足不變式.這是一種具有可組合性的驗證方法:每個并發任務可以單獨進行驗證,只要任務對共享數據的訪問滿足不變式,任務之間自然具備無干擾性.然而,如同 Floyd-Hoare邏輯不支持指針和內存數據結構一樣,該方法也不支持帶指針和內存數據結構的并發程序.并發分離邏輯[100]是結合分離邏輯思想對這種Owicki-Gries方法的擴充,實現對帶指針和內存數據結構的并發程序的模塊化驗證.它充分利用了分離邏輯中的分離合取能夠方便地描述內存空間分離這一特點,將內存從邏輯上分為共享內存以及每個任務自己的私有內存,并要求不同內存之間是分離的.這時,針對共享數據的不變式便只需要描述共享數據自身,而無需描述內存的其他部分.

關系型程序邏輯是對Floyd-Hoare邏輯從一個新的角度進行的擴展,它可以驗證兩個程序之間的關系,或者一個程序在兩種輸入下的行為之間的關系.前者可用于程序精化的驗證,而后者則可用于信息安全性質,例如信息流控制(information flow control)機制的驗證.Benton[158]和 Yang[159]較早提出關系型程序邏輯.Beringer和Hofmann提出將關系型程序邏輯應用于信息流控制[160].Bathe在關系型程序邏輯方面開展了較多研究,主要將其應用于信息安全性質驗證[161].Turon等人[162]和Liang等人[163]提出了關系型程序邏輯開展并發程序的精化驗證.作為對關系型程序邏輯的擴展,Sousa和Dillig提出了笛卡爾霍爾邏輯,用于驗證k-safety,即,程序k次不同執行之間的關系[164].

按照證明方式和自動化程度的不同,基于定理證明的驗證又可以分為兩類,即基于自動定理證明器的自動驗證和基于人機交互的半自動驗證.

3.1.1 基于自動定理證明器的自動驗證

近年來,隨著自動證明理論的發展和計算機處理器能力的大幅增強,自動定理證明器的能力得到大幅提升,基于自動定理證明的驗證也得到很大發展.目前常見的程序證明器(program verifier)包括Dafny[165]、Why3[166]、VeriFast[167]、Smallfoot[168]等.這些程序證明器大多基于某種具體的程序邏輯.給定程序及其規約,證明器能夠自動決定針對程序的每條語句使用程序邏輯中的何種公理或規則,并產生相應的驗證條件作為證明義務.最終,產生的驗證條件被送到自動定理證明器中,由定理證明器完成對驗證條件的證明.目前使用最廣泛的定理證明器是微軟開發的Z3[42],其他常見的證明器還包括CVC4[43]、Yices 2[169]等.

使用各種定理證明器和自動化程序驗證技術,人們已經實現了對一些相對實用的、較大規模的具體系統的驗證.具體工作包括微軟研究院 Hawblitzel等人對操作系統內核、分布式系統等系統的驗證[170,171].Hawblitzel等人將源程序翻譯到中間語言 Boogie[172],在 Boogie上開展驗證,并將生成的驗證條件交給 Z3自動證明.近年來,類似的工作還包括華盛頓大學對操作系統內核[173]和文件系統[174]的自動驗證工作.

基于自動定理證明的驗證工作的優點在于驗證的效率較高,不需要人手工寫證明.然而,由于自動定理證明中很多問題是不可判定問題,而且各個定理證明器又有各自的能力限制,因此能夠表達和證明的性質有限.為了能夠實現自動證明,很多時候需要對待證明的性質和待驗證的代碼本身都進行重寫,甚至為了遷就驗證的自動化而犧牲待驗證的性質以及代碼的功能.例如,在對操作系統內核的自動化驗證工作[173]中,為了實現“一鍵完成(push button verification)”這一特性,內核中帶有循環語句的代碼都被移到了內核外部,從而這部分代碼不再屬于自動化驗證的目標.

3.1.2 人機交互的半自動化證明

基于定理證明的另一類驗證工作,則不強調使用計算機實現驗證的自動化,而是利用計算機來解決證明在計算機中的表示問題以及自動檢查證明的正確性的問題,證明的構造則由人手工和機器交互,以半自動化的方式完成.很多輔助定理證明工具,如Coq[40]和Isabelle/HOL[45]等,都是針對這一目的進行開發的.這類工具往往是利用類型系統和邏輯之間的 Curry-Howard同構關系[146],將構造證明的過程轉化為編寫程序的過程,而證明的正確性檢查也變成了類型檢查問題.

這類人機交互的半自動化驗證工作往往需要大量的手工勞動來構造證明,雖然在輔助定理證明工具中提供了一些基本的證明策略(tactics)和引理庫來減少證明負擔,但在實際代碼的驗證中,往往平均一行程序需要手工書寫 20～30行證明腳本.然而,這種方法的優點在于無需犧牲規約和代碼的表達能力,特別是程序規約可以用表達能力很強的邏輯(如在Coq和Isabelle/HOL中使用的高階邏輯)來表示.而且證明自身在機器中有顯式表示,其正確性可以被自動檢查,因而我們無需依賴自動定理證明算法的正確性,驗證的結論也就更加可信.

3.2 模型檢驗

定理證明中,形式驗證把待證明的性質直接作為了一個數學定理來證明,也稱為演繹式驗證.與演繹式相對應的一種方式是模型檢驗[175-177].模型檢驗分別由Clarke和Emerson、Queille和Sifakis在1980年代初各自獨立提出[19,176],其基本思想是:檢驗一個結構是否滿足一個公式要比證明公式在所有結構下均被滿足容易得多,進而面向并發系統創立了在有窮狀態模型上檢驗公式可滿足性的驗證新形式[178].

模型檢驗通過自動遍歷系統模型的有窮狀態空間來檢驗系統的語義模型與其性質規約之間的滿足關系,其基本框架如圖3所示.模型檢驗中最常見的是時序模型檢驗或邏輯模型檢驗,其系統規約大多是基于模型的規約,使用操作語義描述系統行為,形式模型使用自動機、標記遷移系統等;待檢驗的性質是用時序邏輯描述的基于性質的規約.如果系統模型不滿足性質,模型檢驗算法會給出系統行為不滿足性質規約的反例,用戶可以根據反例進行分析和調試;如果模型檢驗未發現反例,則系統一定滿足所檢驗的性質.

Fig.3 Framework of model checking圖3 模型檢驗框架

3.2.1 基本途徑

模型檢驗的核心是有窮狀態空間上的遍歷策略和算法,主要有顯式方法和隱式方法.顯式方法是通過狀態計算來遍歷狀態空間,隱式方法是通過不動點計算來遍歷狀態空間.兩者的本質都是有窮狀態空間的窮盡搜索.因而,模型檢驗的關鍵問題就是如何應對系統狀態爆炸,在可表示的狀態空間和有效的時間內完成搜索.對于這個問題,主要有3類途徑[179].

(1) 結構化方法:利用定義系統的語法表達(模型)結構來緩解狀態空間爆炸問題,典型的方法有對稱模型檢驗[180-182]、On-the-fly的狀態空間搜索[183,184]、偏序模型檢驗[185-187]、參數化模型檢驗[188,189]等等;

(2) 符號化方法:將模型的遷移結構的狀態和遷移編碼為邏輯公式,這種符號化編碼能夠有效壓縮表示狀態集合的數據結構,狀態變遷的操作也相應高效.符號化的編碼方法常常基于BDD[190]、命題公式[191]或者無量詞的一階約束[192]等等;

(3) 抽象方法:將復雜系統的狀態空間結構歸約為較小的同態映像,后者是前者的一個上近似(overapproximation),從而把原系統的驗證轉化成模型檢驗可以處理的問題[193],例如謂詞抽象方法等.而作為一種更一般化的方法,抽象解釋是一種基于序集合上單調函數對程序形式語義進行可靠近似的理論,為程序自動分析提供了一個通用的框架[194,195].

模型檢驗的其他途徑還包括基于自動機理論的模型檢驗,Vardi和Wolper提出可以基于ω-自動機來進行自動驗證[184].時序邏輯模型檢驗問題可以歸結為基于自動機理論的模型檢驗.在這個途徑中,時序邏輯性質自動轉換為一個自動機,這樣,系統和性質都建模為自動機,模型檢驗問題就歸結為自動機的語言包含、判空等問題.SPIN模型檢驗工具就是基于這種方法.

模型檢驗在建立了系統模型和性質描述后,驗證過程是自動的,并且在證偽時能夠給出調試用的反例.它對于并發系統的驗證比較有優勢,而且可以在不同抽象層次的模型上應用,性質規約也往往是部分規約,可以在系統設計全周期使用.但是它要求模型是有窮狀態空間的,或者能夠在驗證中轉換到有窮的狀態空間抽象上,這在一定程度上限制了模型檢驗的應用.無窮狀態系統的模型檢驗在相當一部分重要的應用場景是可行的,其基本思路是利用符號化方法或數據抽象的方法將無窮狀態系統轉換為一個“性質等價”的有窮狀態表示系統的抽象[196-198].例如實時時序邏輯性質的模型檢驗問題,由于時鐘變量是稠密的,實時系統模型(時間自動機)的狀態空間是無窮的,模型檢驗時用 Region來抽象系統狀態的集合,建立基于 Region的狀態變遷系統,用來遍歷狀態空間以檢驗性質[199].典型的實時模型檢驗工具有 UPPAAL[200].但是,實時模型檢驗的可擴展性仍然是所面臨的巨大挑戰.

實際系統中存在不確定性,這在信息物理融合系統是固有的,例如系統中物理部件的信息感知不穩定、傳輸丟失等等.在這些系統模型的描述中,通過引入概率或者隨機元素來表達系統的不確定性,并在設計策略中,通過容錯、容變機制來獲得期望的量化性質.這類系統量化性質的模型檢驗有兩種途徑.

· 概率模型檢驗[201],其在系統(例如標記變遷系統)中引入概率遷移,采用可描述隨機行為數學結構(例如馬爾可夫鏈)為形式語義,通過數值計算的方式檢驗此類系統是否滿足所期望的概率時序邏輯性質(例如,系統在給定時間內完成相應功能的概率).典型的概率模型檢驗工具有PRISM[202];

· 統計模型檢驗[203,204],其模擬有窮多次的系統執行,然后通過假設檢驗來推斷這些樣本是否提供了統計證據以表明系統滿足或違反性質.

概率模型檢驗的復雜度高;統計模型檢驗避免了窮盡搜索,但其結果具有一定的置信區間.

3.2.2 軟件模型檢驗

軟件系統屬于無窮狀態系統,即使狀態有窮,其狀態空間規模也往往遠超當前計算機可處理的范圍.在硬件系統模型檢驗取得巨大成功的時候,軟件模型檢驗所面臨的挑戰依然嚴峻.對于無窮狀態系統,符號化可達性分析都可能不終止.軟件模型檢驗的核心問題是如何建立規?？蓹z驗的軟件模型(抽象).給定軟件S及待驗證的性質p,抽象模型檢驗就是建立一個抽象映射α,并建立S?p(即S滿足性質p)和α(S)?p的關系.若S?α(S),則稱α(S)為S的上近似(over-approximation);如果α(S)?S,則稱α(S)為S的下近似(under-approximation).

我們可以知道:當抽象不滿足性質,得到的反例一定是真的反例.但是,抽象滿足性質不能得到軟件行為滿足性質,故下近似往往用于調試.如果采用上近似,我們可以知道,當抽象滿足性質就可以得到軟件行為一定滿足性質,但是當抽象即使證偽,得到的反例不一定是真的違反了性質的軟件行為,可能是偽反例.如果不能成功地檢驗得到抽象滿足性質且不能成功找到可行反例,則說明建?？赡苓^于抽象了.軟件模型檢驗要獲得足夠精確的上近似,需要通過抽象精化的方法得到更為精確的模型,而且這個過程能夠通過偽反例的信息來指導獲得,這就是軟件模型檢驗的反例制導的抽象精化方法(CEGAR)[205,206],如圖4所示.

當模型檢驗抽象得到反例時,首先檢驗反例路徑是否是可行的,這通常通過基于反例路徑的編碼約束求解得到.如果不是可行的,即反例的路徑公式是不可滿足的,基于語法的精化就可以通過加減合適的謂詞進行抽象精化.該方法的精化局限于程序中顯式可刻畫的關系.另外一種精化方法是基于插值的方法,通過 Craig插值發現可驗證待驗證安全性質的隱含關系的謂詞.基于插值的方法能夠獲得比基于語法的精化更高的效率.基于抽象精化的模型檢驗工具有SLAM[207]、Blast[208]、CPA checker[209]等等.對于無窮狀態的軟件模型,還可以通過編碼為Horn短句形式求解來進行模型檢驗[210,211].

與一般意義上的模型檢驗不同,限界模型檢驗[191,212,213]通過對模型參數限界,即將模型空間爆炸涉及的參數(例如循環次數、并發數等)限制在一定范圍內,驗證系統模型在此深度內是否滿足系統規約.具體做法是:將系統在有限步長內的行為編碼成一組約束,然后使用約束求解器(例如SAT、SMT求解器)檢驗是否存在相應可行的行為.需要注意的是,限界模型檢驗已經把模型語義改變了,因此即便限界模型檢驗沒有發現錯誤,也并不嚴格保證原系統在參數限定范圍之外的行為也一定滿足所檢驗的性質.隨著約束求解技術的提高,限界模型檢驗方法得到較大范圍的應用.這主要有兩方面的原因:一方面,限界模型檢驗著眼于發現系統中的問題,證偽時保持了模型檢驗能夠反例發現的特點;另一方面,經驗表明,系統的缺陷往往在較小的深度就可以檢測出來.同時,限界模型檢驗方法中也可以綜合應用基于數據約減和控制約減的方法,提高了可擴展性.限界模型檢驗在軟件自動驗證中是常見的途徑,尤其是在并發程序的模型檢驗中.在目前的 SV-COMP并發組比賽中,限界模型檢驗方法具有絕對的優勢[214].它的優點在于避免了開銷大的不動點計算、較高的錯誤發現效率、不需要處理不變式,并且可以根據計算資源能力調整驗證的限界值.然而其不足也很明顯,方法上它不是可靠的.從提高系統可信的角度上看,限界模型檢驗是一種簡單、有效的復雜軟件自動檢驗方法.

在軟件模型檢驗中,利用靜態分析、符號執行等方法抽取程序模型,以及基于路徑的模型檢驗等靜態和動態結合的方法,也是有效提高模型檢驗擴展性的重要途徑[3].近年來,將模型檢驗與定理證明有效地結合也是一個有前景的方向.

4 形式化方法的應用

形式化方法在工業界硬件系統設計應用上十分成功.1992年,Clarke團隊利用SMV驗證了IEEE Futurebus+標準896.1-1991中Cache一致性協議.協議用SMV輸入語言(規約語言)建模,然后使用SMV驗證規約行為(遷移系統)是否滿足 Cache一致性的性質規約,結果發現了一些過去未發現的潛在錯誤[215].SRI和 Rockwell Int’l合作使用PVS系統,規約和驗證了209條AAMP5指令中的108條,驗證了11條代表指令的微碼,發現了微處理器設計中若干微碼的錯誤[216].1994年出現的Intel Pentium浮點單元中的缺陷產生了巨大的影響,促使了形式化方法在硬件工業界的使用.Intel的Kaivola團隊在Intel Core i7驗證項目中,利用形式化方法,花費了約20人年驗證了Core execution cluster,在Intel建立了算術功能驗證的金標準,并為其他CPU和GPU的項目所采納[217].該項研究獲得了2013年的Microsoft Research Verified Software Milestone Award.20世紀90年代后,形式化方法,特別是模型檢驗在硬件設計驗證上的成功,效果得到了工業界的認可.其主要原因是:系統邊界相對清晰、模式較為明顯、動態性不強以及本質上狀態空間有窮.隨著計算能力的提高,形式化方法能得到較好的費效比.

軟件形式化方法的應用比硬件要早,但在工業界的影響要小很多,其主要原因是軟件系統的復雜性遠高于硬件,相應的軟件系統形式化工具水平也遠低于硬件形式化工具,特別是在形式驗證工具方面.即使如此,形式化方法也得到了一些具有顯示度的應用.一個早期的成功案例是,在IBM CICS(客戶信息控制系統)項目中,采用Z方法來描述這個大型交易處理系統的部分系統的規約,結果顯示,與傳統的開發方法相比,開發成本降低了9%,而在開發后期發現的錯誤數量減少了一半左右[218].這是一個對遺留系統進行形式規約重新開發的例子.在軟件開發中,使用形式規約保證系統質量的例子還包括丹麥數據中心DDC在1980年代利用形式化方法開發的ADA語言編譯系統,該系統成為了一個長期服役的商用產品[219].B方法使用在了Paris地鐵的14號線系統和Paris Roissy機場無人駕駛線系統的關鍵部分中,大約占整個軟件系統的三分之一[220].Tokeneer ID Station是Altran Praxis為美國 NSA開展的項目,該項目希望通過實證研究來驗證通過 CC高等級安全測評、ISO/IEC 15408計算機安全認證是否經濟可行.它可以看作是一個關于生產率和質量的對照實驗.在這個小規模的安全系統中,形式規約使用的是Z語言,設計和形式規約精化使用的是INFORMED過程,實現語言是SPARK Ada,驗證工具是 SPARK工具集,并使用自頂向下的系統測試[221].Tokeneer項目是工業界有效應用軟件形式化開發的成功案例,該項目獲得了2011年Microsoft Research Verified Software Milestone Award.

形式化方法應用在工業界的影響不斷增大,自2001年,形式化方法工具獲得了4次ACM軟件系統獎,包括SPIN(2001)、The Boyer-Moore Theorem Prover(2005)、Statemate(2007)、Coq(2013).形式化方法的實踐和相關經驗可參見綜述性文獻[220].

由于形式化方法本身是有開銷的,故在應用中合理考量其應用的經濟性是必須的.形式化方法在安全攸關的系統(航空、航天、核、鐵路等領域)中往往得到較多的應用,一些軟件安全性保證標準,例如DO-178B、DO-178C、DO-333、Common Criteria、SIL1-4都在最(較)高層對系統開發中使用形式化方法提出了要求.美國JPL飛行軟件團隊使用SPIN模型檢驗器及其C代碼模型抽取擴展,分析了火星科學實驗室任務(MSL)中多線程代碼的競爭條件,這些代碼有 120個并行任務在實時操作系統控制下運行[222].在國家自然科學基金委員會“可信軟件基礎研究”重大研究計劃的資助下,我國首次建立了結合形式化方法、覆蓋軟件研制全周期、以可信要素為核心的航天嵌入式軟件可信保障技術體系以及相應的可信保障集成環境,并在“嫦娥”等重大工程軟件的可信性保障中發揮了重要作用[55].有趣的是,人們時常在高等級安全標準中通過形式化方法發現其中的錯誤.例如,通過形式驗證發現了ARINC653 P1-3的6個功能安全問題[223].除了功能安全之外,面向信息安全的形式化方法應用也受到關注,幾乎所有的形式化方法,例如定理證明、模型檢驗、符號執行、抽象解釋在軟件安全、可信平臺等方面都有應用.Subramanyan等人形式化定義了支持可信計算硬件平臺(包括 Intel SGX和 MIT Sactum)的統一抽象模型TAP (trusted abstract platform),形式化定義了TAP所需要滿足的3種關鍵性質,并驗證了Intel SGX和MIT Sactum與TAP之間的精化關系[224].

根據形式化程度的不同,形式化方法應用首先要確定是在整個系統應用亦或在關鍵部分應用.確定了應用的系統范圍或邊界之后,可在相關部分中不同程度地應用形式化方法.一個基本要求是,這些部分都將建立形式規約,而開發中規約精化過程可以有所區分,規約與性質的關系可以通過非形式的說明、嚴格的討論、形式驗證等不同的形式加以論證.質量、生產率和成本是 3個相互制約的因素,形式化方法的應用能夠提高軟件的可靠性和安全性,同時,在當前的技術和工具水平下,也存在著較大的開銷.過度使用形式化方法會使得方法應用的性價比降低,形式化使用程度需要與費效比有一個權衡,這與軟件工程經濟學一樣不可忽視.形式化方法的語用很重要,包括誰來用、使用對象、何時用以及如何用的指南.為提高方法應用的性價比,在形式化方法研究和應用中,領域特定的特點比較突出,往往是應用在部分關鍵模塊,并使用一些其他方法和形式化方法相結合的輕量級形式化方法.

計算機系統軟件自身的可靠性、安全性是整個計算機系統能夠正常工作的前提,因而用形式化方法來驗證系統軟件、為其可靠性和安全性提供嚴格保證,一直是人們長期關注的應用方向.早在 20世紀 80年代,Moore等人就開展了對CLI軟件棧(CLI stack)的形式驗證[225].CLI軟件棧自上而下包括一個編程語言的編譯器、匯編器、鏈接器、一個多任務的操作系統內核以及硬件體系結構.驗證工作涵蓋了上述整個軟件棧,并且構造了抽象層次,使得高層的驗證工作基于低層抽象完成,整個驗證工作形成了一個整體.近 10多年以來,基于交互式定理證明的形式化方法在可驗證的系統軟件上取得顯著的突破.這有 3方面的因素:一是基礎軟件在整個信息系統體系中的價值日益提高,這在一定程度上使得重量級的形式化方法在其上應用的成本變得有可能接受;二是系統軟件與應用軟件相比,其核心部分的邊界和功能比較穩定而不多變,一次驗證完成后可以為社區共享;三是形式驗證工具的自動化能力有了明顯改善,并且系統軟件也可以作為形式化方法發展的磨刀石.在編譯器方面,CompCert始于2005年,一直持續至今,形式驗證了一個基本上符合ISO-C-90和ANSI-C標準的工業級的C語言編譯器,它可以有效生成 PowerPC、ARM 和 x86處理器上的代碼.整個驗證工作集中在編譯過程核心部分,涉及了 14遍掃描和 11種中間語言.CompCert C編譯的驗證規模在當時是空前的,該項研究獲得了 2012年Microsoft Research Verified Software Milestone Award.比較有代表性的操作系統內核驗證則包括澳大利亞NICTA對seL4的驗證[59]、耶魯大學團隊對CertiKOS的驗證[157]、中科大團隊對μC/OS-II的驗證[226]等.seL4在DARPA HACMS項目實驗中,作為無人機系統OS抵御了信息安全攻擊.此外,還有對分布式系統的驗證[227]、安全系統的驗證[228,229]、文件系統的驗證[230,231]等.在系統軟件上的成功,鼓勵了形式化方法在計算機全棧系統形式驗證的努力.2016年,美國 NSF支持了大規模的探索項目DeepSpec,擬形成一種形式化方法開發的全棧工具鏈.

形式化方法不僅能夠保證系統軟件自身的可靠性和安全性,它反過來也能為系統結構的優化提供重要啟發和支持.微軟研究院的Singularity項目團隊指出[232,233]:操作系統中經典的虛擬內存機制其實是一種動態防護機制,防止一個進程的內存錯誤或惡意進程會影響內核或者其他進程.然而,高級程序設計語言的類型安全機制已經能夠確保通過類型檢查的程序不會發生內存錯誤,而且攜帶證明代碼(proof-carrying code,簡稱PCC[234])和帶類型的匯編語言(typed assembly language,簡稱TAL[235])則能確保這種內存安全不僅在源程序上可以保證,在可執行代碼層面依然可以保證.有了這種保證,我們就不再需要虛擬內存機制所提供的保護,從而可以減少為實現虛擬內存所做的動態地址翻譯帶來的運行時開銷.

5 形式化方法面臨的挑戰與未來

具有數學基礎的方法或者建立方法的數學基礎是工程方法走向成熟、理性的必由之路.從應用上看,不斷增加軟件開發的機械化和自動化程度,提高軟件的質量和生產率、盡可能減低成本是工程實踐的愿景.盡管形式化方法對于提高軟件質量的作用已經形成共識,但其對大規模軟件生產率和成本的影響還沒有明確的認識,對形式化方法的認可度和應用度的進展仍然緩慢.在已有的形式化方法的規模應用中,使用者大多是有良好形式化方法素養/培訓的人員,甚至是方法、技術和工具本身的研發者.一些軟件工程實踐表明:除了把程序視作形式規約以外,工程師們并不愿意大量編寫形式規約,認為形式化方法本身比較復雜,在某種程度上增加了軟件系統的設計復雜度.因此,形式化方法的首要挑戰是發展形式化方法的應用形態,包括技術形態和工具形態,提高形式化方法的易用性、有效性和擴展性,降低形式化方法的應用門檻.

程序設計語言和程序正確性是形式化方法發展的最初源泉.面向程序設計語言和代碼,研究和運用形式化方法、技術與工具是一個重要的方向.人們在實際的程序設計語言上開展了很多驗證技術的研究,圍繞程序代碼的形式驗證技術的發展趨勢將會明顯,驗證將成為程序設計環境的一部分,如同程序測試、代碼推薦的功能一般.程序設計語言與規約語言的融合將成為趨勢.形式化方法的許多思想和方法在程序設計語言的設計中有重要的影響.許多新型程序設計語言設計之初的想法和應用源自于形式化方法.Rust語言[236]的成功是形式化方法研究對系統開發提供支持的代表性案例,它主要面向系統編程:一方面,語言支持并發以及手工內存分配和釋放;另一方面,語言借鑒類型系統、線性邏輯和并發分離邏輯的思想,在語言中引入內存所有權(ownership)以及所有權傳遞(ownership transfer)的概念,避免了內存錯誤以及并發程序中常見的數據競爭錯誤.目前,Rust語言受到了工業界和學術界的廣泛關注,已有多個使用Rust開發的較有影響力的系統,包括瀏覽器、操作系統和其他各種工具.與這一趨勢相伴,對可視化編程機制以及領域相關特性的支持,將進一步推動新型語言的可用性和可行性.

近 10年來,形式化方法進入一個振興的階段.無論是輕量級的形式化方法與主流方法的結合,還是重量級的形式化方法在工業級軟件上的應用,都取得了較大的進步和成功[237].在這些成功應用的后面,工具起到了決定性的作用.系統一旦使用了形式規約語言建模,它就能用工具進行語義分析.工具也緩解了問題規模帶來的壓力.因此,構建更加可用和魯棒的工具支持大規模規約的并行語義分析和驗證,構建可復用的形式規約庫和方法社區,推動形式化方法工具和可復用庫設施的進步,包括工具的集成、工具的無形化、規約與驗證資產,毫無疑問都會是形式化方法努力的方向.

規約、開發和驗證的系統與環境的形態變化是形式化方法發展的驅動力.形式化方法的目標在于高質量的描述、開發和確認軟件系統,因而軟/硬件的形態進步和地位的變化對形式化方法有著直接的影響.例如,形式化方法發展的一條重要線索是從順序程序到并行程序、混成系統、信息物理融合系統乃至人機物融合系統,而人機物融合社會中混成系統對形式化方法的基礎、方法、技術和工具都形成了全面的挑戰[238,239].

軟件正在成為社會基礎設施,而形式化方法在計算機系統基礎軟/硬件的可靠性中發揮了十分重要的作用,這正是人們最能認識到的形式化方法在關鍵的信息基礎設施中發揮作用的應用點.在軟件基礎設施方面,全棧的可驗證軟件將會持續地進展,并有可能在實用主流操作系統中逐漸地滲透.例如,為了保證云服務基礎設施的可靠性,Amazon利用TLA+方法對其S3云存儲服務的關鍵算法進行了形式驗證,發現了不少缺陷[240].2017年,Linux基金會宣稱,將對一些 Linux內核模塊進行形式驗證以提高系統的安全性[241].基于形式化方法的信息安全性研究毫無疑問是一個方向[242].面向未來的軟件基礎設施,區塊鏈和智能合約的正確性及信息安全性驗證正蓬勃展開[243,244].

在軟件定義一切的時代,形式化方法將定義軟件.形式化方法如何與其他軟件開發方法、領域特定的融合顯得尤為重要.對應于軟件定義時代的軟件形態的特征變化、質量的需求變化,形式化方法需要在基礎概念、規約、開發和驗證技術與工具上適應更為復雜開放、動態多變、持續演化的軟件形態.例如,在人機物融合下,需要準確、恰當地處理非形式化需求到形式規約、形式化抽象到非形式化場景和現實世界的邊界建模,大量非功能規約包括社會化人因的規約,自主自適應自組織等新型軟件結構和行為的規約、推理與驗證等等.在形式化方法的發展中,數學與形式化方法有著密切的互動,數學為形式化模型和推理提供了基礎,而形式化方法也促進了數學的發展.形式化方法可以機械、高效、準確無誤地寫出復雜數學問題的可靠證明,甚至幫助解決一些長期懸而未決的數學難題,例如四色定理[245]、羅賓斯猜想(Robbins conjecture)[246]、開普勒猜想(Kepler conjecture)[247](該原始證明超過 300多頁,正式發表的證明也近 130頁,其正確性無法保證[248])等等.形式化(工程)數學[249]對于構建高可信智能制造軟件環境也具有重要價值.

形式化方法和人工智能有著密切的聯系.定理證明和約束求解是符號主義流派人工智能的重要內容.如何利用人工智能的其他成果提高形式化方法的水平是一個值得關注的方向,例如基于機器學習幫助構建形式規約、發現不變式或者推薦證明策略輔助形式驗證、輔助規約精化和程序綜合等等.程序綜合與機器學習交叉,出現了基于深度學習和框架生成相結合的程序綜合方法.另一方面,機器學習軟件也是程序,研究它們的形式化方法是非常有價值的[250,251].例如,概率程序設計的形式語義、驗證和調試、大數據處理程序的驗證、深度學習程序的形式規約與魯棒性驗證、利用形式化方法建立更好的訓練方法、研究機器學習的可解釋性,都是值得探索的課題.

在新的計算模型方面,量子程序設計[252]的理論成為了形式化方法發展的新內容.形式化方法已經應用到了量子程序設計語言的語義分析、關鍵性質的推理,也出現了量子計算的程序邏輯和模型檢驗方法.由于量子程序和傳統程序相比有很大的不同,特別是由于量子疊加和糾纏的存在,建立系統的量子計算的形式化方法并開發有效的驗證技術才剛剛起步.

計算思維的滲透性也帶動了形式化方法與其他學科的交叉融合,例如在生物研究領域,計算建模和分析已經成為一種重要方法[253],例如Na?ve T cell differentiation的時序行為建模和分析[254].這些研究有力地促進了混成系統形式化方法的發展,也促進了醫療生命科學的發展,并為醫工結合交叉提供了一個明確的方向[255].

教育是形式化方法持續發展的重要推手.受限于可用性和可擴展性,形式化方法學習曲線長,高強度運用需要較高的門檻,嚴重制約了形式化方法在軟件開發中的廣泛應用.而計算系統的可信愈來愈重要,ACM 和 IEEE制定的計算機科學和軟件工程課程計劃都包含了程序正確性的內容[256,257].我國的形式化方法教育現狀調查結果指出,需要加強專業教育中形式化方法認知[258].形式化方法的輕量級運用已經能夠顯著提高人們對系統需求和設計的理解,而且程序就是一種形式規約,可以機械化自動地處理(編譯或執行).形式化方法對于軟件開發人員而言實際上都在接觸,只是形式化程度不同而已.因而在計算思維養成過程中,在程序設計、數據結構等基礎課增加形式化概念的討論,在離散數學、算法、軟件工程等后續專業課程突出形式化方法與主流方法的關系和結合,對于形式化方法的推廣和水平提高是非常重要的.

6 結束語

形式化方法可以嚴格分析、處理、證明計算機系統和程序及其性質,對于確保系統正確性和提高可信性具有基礎性的作用.形式化方法的應用已經取得了長足的進步,實踐證實,其在大規模程序設計中起到了一個直接的指導作用,提供了形式化開發的概念框架和基本理解,促進了目前的最佳實踐,其成果深刻影響了未來軟件學科的發展方向[259].同時,形式化方法需要適應軟件定義使能的軟件新形態,適應軟件作為社會基礎設施的地位,在基礎概念、規約、驗證和工具等方面進一步發展,并與人工智能、網絡空間安全、量子計算、生物計算等領域和方向交叉、融合.

致謝感謝成文過程中周巢塵、林惠民院士的指導,劉波、劉江潮博士以及安杰、李朝暉、王健同學的幫助.