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

1(國(guó)防科技大學(xué) 計(jì)算機(jī)學(xué)院,湖南 長(zhǎng)沙 410073)

2(高性能計(jì)算國(guó)家重點(diǎn)實(shí)驗(yàn)室(國(guó)防科技大學(xué)),湖南 長(zhǎng)沙 410073)

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

4(天基綜合信息系統(tǒng)重點(diǎn)實(shí)驗(yàn)室(中國(guó)科學(xué)院 軟件研究所),北京 100190)

5(南京大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)系,江蘇 南京 210023)

6(計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室(南京大學(xué)),江蘇 南京 210023)

7(西南大學(xué) 計(jì)算機(jī)與信息科學(xué)學(xué)院,重慶 400715)

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

計(jì)算機(jī)科學(xué)的發(fā)展主要涉及硬件和軟件的發(fā)展,而軟、硬件發(fā)展的核心問(wèn)題之一是如何保證它們是可靠的、安全的,關(guān)鍵問(wèn)題是正確性.如今,硬件性能變得越來(lái)越高、運(yùn)算速度變得越來(lái)越快、體系結(jié)構(gòu)變得越來(lái)越復(fù)雜,軟件的功能也變得越來(lái)越強(qiáng)大而復(fù)雜,如何開(kāi)發(fā)可靠的軟、硬件系統(tǒng),已經(jīng)成為計(jì)算機(jī)科學(xué)發(fā)展的巨大挑戰(zhàn).特別是現(xiàn)在計(jì)算機(jī)系統(tǒng)已廣泛應(yīng)用于許多關(guān)系國(guó)計(jì)民生的安全攸關(guān)系統(tǒng)中,例如高速列車控制系統(tǒng)、航空航天控制系統(tǒng)、核反應(yīng)堆控制系統(tǒng)、醫(yī)療設(shè)備系統(tǒng)等等,這些系統(tǒng)中的任何錯(cuò)誤都可能導(dǎo)致災(zāi)難性后果.

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

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

本文主要給出形式化方法的基本方法學(xué)和發(fā)展概貌,第1節(jié)介紹形式化方法的基本概念、簡(jiǎn)要?dú)v史和構(gòu)成體系.第2節(jié)、第3節(jié)分別介紹形式規(guī)約和開(kāi)發(fā)以及形式驗(yàn)證的基本內(nèi)容和現(xiàn)狀.第4節(jié)介紹形式化方法的應(yīng)用.第 5節(jié)討論形式化方法面臨的一些挑戰(zhàn),展望其在軟件逐漸成為基礎(chǔ)設(shè)施時(shí)代的發(fā)展趨勢(shì)和交叉方向,并給出一些加強(qiáng)形式化教育的建議.

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

1 形式化方法基本概念

形式化方法是基于嚴(yán)格數(shù)學(xué)基礎(chǔ),對(duì)計(jì)算機(jī)軟(硬)件系統(tǒng)進(jìn)行形式規(guī)約、開(kāi)發(fā)和驗(yàn)證的技術(shù).其中,形式規(guī)約使用形式語(yǔ)言構(gòu)建所開(kāi)發(fā)的軟件系統(tǒng)的規(guī)約,它們對(duì)應(yīng)于軟件生命周期不同階段的制品,刻畫(huà)系統(tǒng)不同抽象層次的模型和性質(zhì),例如需求模型、設(shè)計(jì)模型甚至代碼和代碼的執(zhí)行模型等.形式驗(yàn)證是證明不同形式規(guī)約之間的邏輯關(guān)系,這些邏輯關(guān)系反映了在軟件開(kāi)發(fā)不同階段軟件制品之間的需要滿足的各類正確性需求.例如,形式驗(yàn)證給出“系統(tǒng)設(shè)計(jì)模型滿足若干特定性質(zhì)”的證明構(gòu)造.在形式規(guī)約和驗(yàn)證的基礎(chǔ)上,形式化開(kāi)發(fā)主要是構(gòu)造、證明形式規(guī)約之間的等價(jià)轉(zhuǎn)換和精化關(guān)系,以系統(tǒng)的形式模型為指導(dǎo),逐步精化,開(kāi)發(fā)出滿足需要的系統(tǒng),也稱為構(gòu)造即正確(correct by construction)的開(kāi)發(fā).

形式化方法與其他軟件開(kāi)發(fā)方法[4]的主要區(qū)別在于:其描述軟件及其性質(zhì)的語(yǔ)言是無(wú)歧義的,構(gòu)造和驗(yàn)證軟件的方法是嚴(yán)格的.在軟件工程中,形式化方法提供了工程化系統(tǒng)設(shè)計(jì)的一種比較透徹的思維方式,可以很好地支持抽象模型建立、系統(tǒng)精化、模型和證明重用;形式化開(kāi)發(fā)過(guò)程具有很好的可重復(fù)性,相應(yīng)的軟件制品模型也具有較強(qiáng)的可分析性和可驗(yàn)證性.因而,形式化方法可以有效地提高和保障系統(tǒng)的可信性.

形式化方法與計(jì)算機(jī)科學(xué)理論密切相關(guān),其發(fā)展與程序設(shè)計(jì)語(yǔ)言和程序理論的發(fā)展息息相連.作為一個(gè)學(xué)科方向,它研究形式化方法的數(shù)學(xué)基礎(chǔ)、形式系統(tǒng)的表達(dá)能力、形式系統(tǒng)的推理系統(tǒng)及其可靠性和完備性,以及在計(jì)算系統(tǒng)開(kāi)發(fā)和生命周期各個(gè)階段的理論、方法、技術(shù)、工具和應(yīng)用方式等.

1.1 歷史回顧

形式化方法的發(fā)展已有較長(zhǎng)的歷史,人們主要從兩個(gè)角度出發(fā)推動(dòng)形式化方法的提出和早期發(fā)展,即,為程序設(shè)計(jì)提供數(shù)學(xué)基礎(chǔ)的理論研究角度以及為軟件開(kāi)發(fā)提供嚴(yán)格質(zhì)量保證的軟件工程角度.早在1949年,Turing的論文“Checking a large routine”即討論了程序的正確性問(wèn)題[5].1962年,McCarthy在IFIP上做了題為“通往計(jì)算的數(shù)學(xué)科學(xué)”的演講[6],系統(tǒng)論述了程序語(yǔ)言的形式語(yǔ)義和程序設(shè)計(jì)理論重要性,直接觸發(fā)了形式語(yǔ)義研究.1968年在德國(guó)Garmisch召開(kāi)的NATO軟件工程會(huì)議,從提高軟件質(zhì)量和生產(chǎn)率的軟件工程角度出發(fā),提出了要建立軟件開(kāi)發(fā)和生產(chǎn)的數(shù)學(xué)基礎(chǔ);進(jìn)一步地,軟件的正確性問(wèn)題和概念成為1969年NATO軟件工程會(huì)議的主題之一.形式化方法在這種歷史背景下成為程序設(shè)計(jì)和軟件工程基礎(chǔ)的重要組成部分,先后出現(xiàn)了一批有重要影響的工作.表1給出了部分圖靈獎(jiǎng)獲獎(jiǎng)?wù)咴谛问交椒ǚ矫娴难芯抗ぷ?

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

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

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

1.1.2 圍繞形式規(guī)約和開(kāi)發(fā)的方法學(xué)研究(1970年～至今)

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

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

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

1.1.4 以可驗(yàn)證軟件為目標(biāo)的多學(xué)科交叉研究(2000年～至今)

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

1.2 形式化方法的基本體系

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

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

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

綜上所述,形式化方法是由形式規(guī)約語(yǔ)言(包括形式語(yǔ)義與模型理論)、形式規(guī)約(包括精化與綜合)、形式驗(yàn)證、形式化工具等形成的一個(gè)整體.其中,形式規(guī)約語(yǔ)言是基礎(chǔ),形式化方法中,軟件制品是規(guī)約語(yǔ)言編寫(xiě)/變換的形式規(guī)約;形式驗(yàn)證是保證開(kāi)發(fā)正確性的途徑,形式語(yǔ)義與模型理論是聯(lián)接形式規(guī)約和形式驗(yàn)證的數(shù)學(xué)紐帶;形式化工具是系統(tǒng)設(shè)計(jì)和開(kāi)發(fā)中高效使用形式化方法的需要和實(shí)踐.

2 形式規(guī)約

形式規(guī)約是由形式規(guī)約語(yǔ)言嚴(yán)格描述的系統(tǒng)模型或者系統(tǒng)需要滿足的性質(zhì).前者是模型規(guī)約,后者是性質(zhì)規(guī)約.形式規(guī)約是形式化方法的基礎(chǔ)[64].在軟件分析[2,3]中,動(dòng)態(tài)執(zhí)行測(cè)試或驗(yàn)證技術(shù)以及動(dòng)態(tài)在線跟蹤監(jiān)控和驗(yàn)證也經(jīng)常使用形式規(guī)約.

本節(jié)我們討論形式規(guī)約語(yǔ)言及其語(yǔ)義的定義方法、形式規(guī)約和語(yǔ)義模型之間的關(guān)系,并在此基礎(chǔ)上介紹形式規(guī)約在軟件構(gòu)造中的應(yīng)用.

2.1 形式規(guī)約語(yǔ)言

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

2.1.1 模型規(guī)約語(yǔ)言

模型規(guī)約語(yǔ)言利用數(shù)學(xué)結(jié)構(gòu)描述系統(tǒng)的狀態(tài)變化或者事件軌跡,它直接定義所描述系統(tǒng)模型的結(jié)構(gòu)、功能行為甚至非功能行為(如時(shí)間).模型規(guī)約給出了系統(tǒng)開(kāi)發(fā)過(guò)程中不同抽象層次的模型,有相應(yīng)的邏輯推理系統(tǒng)支持其分解和組合,完成不同層次間規(guī)約的轉(zhuǎn)換和精化.主要包括如下幾類.

(1) 代數(shù)規(guī)約語(yǔ)言

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

(2) 結(jié)構(gòu)化規(guī)約語(yǔ)言

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

為了提供面向?qū)ο蟮能浖?guī)約和精化,VDM擴(kuò)展到VDM++[74],Z擴(kuò)展為Object-Z[75].在VDM和Z的基礎(chǔ)和思想的影響下,為了處理交互的分布式軟件和基于服務(wù)的系統(tǒng),在類似基于數(shù)據(jù)狀態(tài)的VDM和Z的靜態(tài)規(guī)約語(yǔ)言中引進(jìn)了事件和狀態(tài)遷移行為,發(fā)展了一系列的規(guī)約語(yǔ)言,包括 B[76]、Event-B[29]、Alloy[77]、JML[78]和rCOS[34]等,這些規(guī)約語(yǔ)言都有明顯的軟件結(jié)構(gòu)描述,其中,JML和rCOS直接使用了現(xiàn)代高級(jí)程序語(yǔ)言的結(jié)構(gòu)機(jī)制表示軟件架構(gòu),例如面向?qū)ο蟮睦^承和基于構(gòu)件的軟件界面和連接器(connector).

(3) 進(jìn)程代數(shù)(演算)

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

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

(4) 基于遷移系統(tǒng)的規(guī)約

遷移系統(tǒng)可以自然地表示系統(tǒng)的行為.典型的基于遷移系統(tǒng)的規(guī)約語(yǔ)言有Petri網(wǎng)[12]和Statecharts[87]等.基于遷移系統(tǒng)的規(guī)約語(yǔ)言往往有圖形化表示,稱為可視化規(guī)約語(yǔ)言.Statecharts用Higragh進(jìn)行形式定義,圖的節(jié)點(diǎn)代表系統(tǒng)執(zhí)行的狀態(tài),而一個(gè)節(jié)點(diǎn)到另一個(gè)節(jié)點(diǎn)的邊表示從一個(gè)狀態(tài)到另一個(gè)狀態(tài)的遷移,可將模型轉(zhuǎn)化為規(guī)則形式定義,構(gòu)成一個(gè)推理系統(tǒng).由于其執(zhí)行模型是抽象機(jī),這樣的圖形語(yǔ)言可以構(gòu)建可執(zhí)行的規(guī)約(executable specification)或可執(zhí)行的模型(executable model),能夠?qū)ο到y(tǒng)行為進(jìn)行仿真、測(cè)試.它們經(jīng)常作為時(shí)序邏輯的解釋(模型)使用,可以用時(shí)序邏輯進(jìn)行規(guī)約和證明其性質(zhì),也可用算法判定其建立的模型是否滿足一個(gè)時(shí)序邏輯公式.結(jié)果可以作為系統(tǒng)早期設(shè)計(jì)驗(yàn)證的依據(jù),以便盡早發(fā)現(xiàn)設(shè)計(jì)錯(cuò)誤.但是這種形式規(guī)約組合性較差,不容易對(duì)復(fù)雜系統(tǒng)建模.

為了對(duì)非功能性需求建模,人們對(duì)標(biāo)記遷移系統(tǒng)進(jìn)行了各種擴(kuò)充.以自動(dòng)機(jī)為例,其后續(xù)擴(kuò)展包括:時(shí)間自動(dòng)機(jī)[21]、混成自動(dòng)機(jī)[88]、概率時(shí)間自動(dòng)機(jī)[89]、隨機(jī)混成自動(dòng)機(jī)[90],等等.而且這些模型不再局限于計(jì)算機(jī)領(lǐng)域,已經(jīng)廣泛應(yīng)用于控制、生物、物理、化學(xué)等諸多領(lǐng)域.

2.1.2 性質(zhì)規(guī)約語(yǔ)言

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

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

a)部分正確性:如果一個(gè)初始狀態(tài)滿足 Pre,且P由該初始狀態(tài)的執(zhí)行能夠終止,那么終止?fàn)顟B(tài)一定能夠滿足Post;

b)完全正確性:如果一個(gè)初始狀態(tài)滿足 Pre,那么 P由該初始狀態(tài)的執(zhí)行一定能夠終止,且終止?fàn)顟B(tài)一定能夠滿足Post.

Floyd-Hoare邏輯的推理系統(tǒng)是在一階謂詞系統(tǒng)基礎(chǔ)上添加關(guān)于程序的公理和推理規(guī)則來(lái)建立的.類似的規(guī)約語(yǔ)言有Dijkstra的衛(wèi)士命令語(yǔ)言的最弱前置條件演算[94].

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

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

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

2.2 形式語(yǔ)義學(xué)

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

2.2.1 操作語(yǔ)義

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

操作語(yǔ)義是最早使用的形式語(yǔ)義方法,用來(lái)給出順序程序的語(yǔ)義,此時(shí),狀態(tài)均是一些簡(jiǎn)單的數(shù)據(jù)結(jié)構(gòu),遷移關(guān)系一般都是確定的、離散的,也不需要考慮標(biāo)號(hào)間的通信和同步.為了定義復(fù)雜程序的操作語(yǔ)義,例如面向?qū)ο蟪绦?、并發(fā)程序、實(shí)時(shí)程序、概率程序、混成系統(tǒng)等,人們對(duì)遷移系統(tǒng)進(jìn)行了各種擴(kuò)充,或擴(kuò)充它的狀態(tài),或擴(kuò)充它的遷移關(guān)系,亦或兩者同時(shí)擴(kuò)充.例如,為了定義面向?qū)ο蟪绦?人們擴(kuò)充了程序狀態(tài),引入堆和棧等復(fù)雜數(shù)據(jù)結(jié)構(gòu)[121];為了處理并發(fā)程序,人們擴(kuò)充了標(biāo)號(hào)遷移關(guān)系,允許使用標(biāo)號(hào)描述通信和同步[83];為了描述概率和隨機(jī)程序,允許以給定的概率或者隨機(jī)選取遷移規(guī)則[122]等等.

操作語(yǔ)義基于抽象機(jī),與計(jì)算機(jī)最為接近,可描述實(shí)現(xiàn)方面的執(zhí)行細(xì)節(jié),操作性比較強(qiáng),適合于開(kāi)發(fā)語(yǔ)言編譯器以及編譯優(yōu)化的應(yīng)用.在語(yǔ)義中,狀態(tài)是被直接表示和操作的,也比較適用于形式驗(yàn)證中基于狀態(tài)搜索的模型檢驗(yàn)方法里的語(yǔ)義模型.然而,在大規(guī)?；驘o(wú)窮狀態(tài)的系統(tǒng)中,抽象機(jī)上的推理系統(tǒng)比較弱,不易進(jìn)行基于演繹推理的形式驗(yàn)證.

2.2.2 指稱語(yǔ)義

指稱語(yǔ)義(denotational semantics)將語(yǔ)言的基本語(yǔ)法成分解釋成為數(shù)學(xué)對(duì)象(稱為指稱),用數(shù)學(xué)對(duì)象上的運(yùn)算來(lái)定義語(yǔ)言的語(yǔ)義.論域理論是指稱語(yǔ)義的數(shù)學(xué)基礎(chǔ),討論各種語(yǔ)言成分的指稱的數(shù)學(xué)結(jié)構(gòu),并提供數(shù)學(xué)工具,從而在各種數(shù)學(xué)結(jié)構(gòu)之上定義語(yǔ)言語(yǔ)義和推導(dǎo)語(yǔ)言成分特性.例如,將程序語(yǔ)言的基本語(yǔ)法實(shí)體的指稱定義為程序狀態(tài)空間上的函數(shù)和泛函,復(fù)合語(yǔ)法實(shí)體的指稱由構(gòu)成它的子成分的指稱復(fù)合得到.

建立指稱語(yǔ)義的首要任務(wù)是確定一個(gè)相應(yīng)的論域理論,即確定程序語(yǔ)言的解釋域[123].處理不同的計(jì)算現(xiàn)象需要不同的語(yǔ)義,例如,可以定義不關(guān)心是否停機(jī)的順序程序的語(yǔ)義,也可以定義需要刻畫(huà)停機(jī)的語(yǔ)義.顯然,不同的語(yǔ)義需要不同的論域.以CSP為例,Hoare等人提出了CSP的跡語(yǔ)義模型、失效-發(fā)散-跡語(yǔ)義模型等[14,124],這些語(yǔ)義的區(qū)別在于失效-發(fā)散的語(yǔ)義可以刻畫(huà)程序死鎖以及活鎖,從而分析系統(tǒng)的活性.論域理論的研究隨著程序?qū)ο蟮牟煌粩嗟匕l(fā)展著,例如,針對(duì) Timed CSP,人們擴(kuò)充了跡語(yǔ)義模型和失效-發(fā)散-跡語(yǔ)義模型,分別提出了帶時(shí)間戳的跡語(yǔ)義模型和帶時(shí)間戳的失效-發(fā)散-跡語(yǔ)義模型[23,125].

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

2.2.3 代數(shù)語(yǔ)義

代數(shù)語(yǔ)義(algebraic semantics)用代數(shù)結(jié)構(gòu)來(lái)定義計(jì)算機(jī)語(yǔ)言(特別是代數(shù)規(guī)約語(yǔ)言)的語(yǔ)義,是在抽象數(shù)據(jù)類型的基礎(chǔ)上發(fā)展起來(lái)的[118].在抽象數(shù)據(jù)類型中,基調(diào)是用代數(shù)結(jié)構(gòu)描述數(shù)據(jù)類型的語(yǔ)法(類子和類子間的運(yùn)算),運(yùn)算的推導(dǎo)規(guī)則用一組公理(等式或者條件等式)描述,這樣,滿足這組公理的模型就是這個(gè)抽象數(shù)據(jù)類型的一個(gè)代數(shù)語(yǔ)義(稱為∑-代數(shù),其中,∑是基調(diào)).基于代數(shù)語(yǔ)義,可以利用模型論和范疇論方法來(lái)推理該語(yǔ)言的程序性質(zhì).

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

代數(shù)語(yǔ)義與代數(shù)規(guī)約的關(guān)系密切,主要用于解決基于代數(shù)規(guī)約的形式化開(kāi)發(fā)中程序正確性的推理,抽象程度比較高.如果將等式看作是從左至右的重寫(xiě)規(guī)則,代數(shù)規(guī)約就以項(xiàng)重寫(xiě)的形式可執(zhí)行,成為了一種可執(zhí)行規(guī)約.

2.2.4 公理語(yǔ)義

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

最為常見(jiàn)的有基于一階邏輯擴(kuò)展的Floyd-Hoare邏輯、謂詞轉(zhuǎn)換器(predicate tranformer)等.Floyd-Hoare邏輯最初是針對(duì)順序程序提出來(lái)的,并擴(kuò)展至并發(fā)程序、實(shí)時(shí)系統(tǒng)、混成系統(tǒng)甚至量子系統(tǒng)等.面向指針程序和面向?qū)ο蟪绦虍a(chǎn)生了分離邏輯及其變種,這些研究把 Floyd-Hoare邏輯的應(yīng)用真正地推進(jìn)到實(shí)際的程序驗(yàn)證.人們還提出了動(dòng)態(tài)邏輯、模態(tài)邏輯、時(shí)序邏輯等用來(lái)作為定義程序公理語(yǔ)義的形式系統(tǒng).公理語(yǔ)義在形式驗(yàn)證中的應(yīng)用是比較多的.

表2給出了這4種語(yǔ)義之間的一個(gè)比較.程序語(yǔ)言的形式語(yǔ)義的機(jī)器定義是建立形式驗(yàn)證的基礎(chǔ).例如,可以使用定理證明器的元語(yǔ)言來(lái)機(jī)器實(shí)現(xiàn)程序語(yǔ)言的語(yǔ)義,也可直接用函數(shù)式語(yǔ)言來(lái)實(shí)現(xiàn)目標(biāo)程序語(yǔ)言的語(yǔ)義.K框架基于重寫(xiě)的可執(zhí)行語(yǔ)義框架,用來(lái)定義程序語(yǔ)言的操作語(yǔ)義,能夠解釋執(zhí)行程序、空間搜索和模型檢驗(yàn),支持該語(yǔ)言程序的驗(yàn)證[128].基于K框架,定義了C99和Java 1.4的形式語(yǔ)義[128,129].

Table 2 Comparsion of formal semantics表2 形式語(yǔ)義風(fēng)格之間的比較

2.3 形式化開(kāi)發(fā)與軟件構(gòu)造

形式規(guī)約和開(kāi)發(fā)方法遵循軟件開(kāi)發(fā)方法的基本原理,包括關(guān)注點(diǎn)分離和逐步精化.在形式規(guī)約和驗(yàn)證的基礎(chǔ)上,軟件形式化構(gòu)造活動(dòng)包括針對(duì)形式規(guī)約多視角建模、不同抽象層上規(guī)約間的精化以及程序綜合等.

2.3.1 基于規(guī)約的形式化開(kāi)發(fā)

形式規(guī)約必須具有良好的性質(zhì).形式系統(tǒng)的一致性表明其是否語(yǔ)義可滿足,換言之,形式規(guī)約的一致性刻畫(huà)了其是否是可實(shí)現(xiàn)的.即:它對(duì)應(yīng)滿足關(guān)系的語(yǔ)義域非空,說(shuō)明這個(gè)規(guī)約有滿足其約束的實(shí)現(xiàn),理論上是可實(shí)現(xiàn)的.當(dāng)形式規(guī)約用來(lái)描述需求時(shí),則成為判斷需求規(guī)約可行性的重要途徑.另一方面,一般不要求形式規(guī)約是完備的,不完備的規(guī)約可以給實(shí)現(xiàn)者更多實(shí)現(xiàn)方法上的空間,也給了開(kāi)發(fā)人員平衡未來(lái)實(shí)現(xiàn)在功能和性能上的空間.一個(gè)規(guī)約本身就可以有多個(gè)不同的實(shí)現(xiàn),例如實(shí)現(xiàn)的數(shù)據(jù)結(jié)構(gòu)和算法.

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

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

Fig.2 Formal development methods—Multiple views圖2 形式化開(kāi)發(fā)方法——多維視圖

軟件開(kāi)發(fā)過(guò)程中,形式規(guī)約方法與設(shè)計(jì)方法一樣是逐步開(kāi)發(fā)的.以形式規(guī)約為制品的設(shè)計(jì)形成了形式化開(kāi)發(fā)的主線.形式化開(kāi)發(fā)中最重要的設(shè)計(jì)活動(dòng)是精化,它是將形式規(guī)約的抽象層次向?qū)崿F(xiàn)加以變換.例如,一個(gè)層次的模塊分解為下一個(gè)層次的若干模塊,或者具體化一個(gè)抽象數(shù)據(jù)類型的表示類型.精化需要保持正確性,并具有組合性,不同抽象層次逐步開(kāi)發(fā)的形式規(guī)約形成了規(guī)約的精化鏈.基于合約的規(guī)約有很好的可組合性并支持建立精化演算.圖2所示的需求分析結(jié)果可以是系統(tǒng)或構(gòu)件與環(huán)境的合約規(guī)約,而架構(gòu)設(shè)計(jì)中子系統(tǒng)或構(gòu)件C1和C2在各自的合約基礎(chǔ)上加以組合,計(jì)算出組合系統(tǒng)的合約規(guī)約,并保證是上層合約的精化,即保證滿足上層規(guī)約的所有需求性質(zhì).整個(gè)設(shè)計(jì)過(guò)程可以理解為一個(gè)逐步分解和精化的過(guò)程.

精化演算是以組合化方式支持逐步求精的形式推理系統(tǒng),最早是面向順序程序[132,133],近年來(lái)發(fā)展到了反應(yīng)式系統(tǒng)精化[134,135]和構(gòu)件化軟件的精化[34].在形式化逐步求精過(guò)程中,精化都可以是形式化的,每步精化需要證明下一層的規(guī)約滿足上一層的規(guī)約,.在實(shí)際應(yīng)用中,因?yàn)槌杀締?wèn)題,工業(yè)界往往不這么做.但是,有精化演算指導(dǎo)的設(shè)計(jì)過(guò)程無(wú)疑能提高設(shè)計(jì)質(zhì)量.軟件工程中建立的一系列設(shè)計(jì)模式(design pattern)在一定意義上就是對(duì)精化技術(shù)的一種非形式化的工程實(shí)踐.如果在安全攸關(guān)的應(yīng)用開(kāi)發(fā)時(shí)能夠盡可能地形式化,則對(duì)于確保安全性是有顯著意義的.在形式化開(kāi)發(fā)中,精化過(guò)程的一種重要技術(shù)是程序綜合,即,從規(guī)約能夠直接生成程序,參見(jiàn)第2.3.2節(jié).

在逐步求精的過(guò)程中,形式化方法有效支持關(guān)注點(diǎn)分離的軟件工程原則.一般情況下,數(shù)據(jù)功能、交互通信協(xié)議和動(dòng)態(tài)規(guī)約可以分別求精;從無(wú)時(shí)間的規(guī)約到有時(shí)間的規(guī)約一般可以是精化(時(shí)間模型的健康條件)[40],容錯(cuò)也可以視為原來(lái)設(shè)計(jì)規(guī)約的精化[136].另外,基于形式化的設(shè)計(jì)精化一般有很好的可組合性,分解和精化支持模型重用、證明分析過(guò)程重用、代碼重用,所以有效支持分而治之的工程原則,尤其是基于構(gòu)件和服務(wù)化系統(tǒng)的開(kāi)發(fā).

研究、理解和處理軟件開(kāi)發(fā)的復(fù)雜性,一直是驅(qū)動(dòng)軟件工程發(fā)展的核心問(wèn)題.針對(duì)Brooks指出的軟件開(kāi)發(fā)復(fù)雜性來(lái)源[137],形式化開(kāi)發(fā)從需求規(guī)約到軟件代碼,將軟件開(kāi)發(fā)建立在一個(gè)有理論基礎(chǔ)和規(guī)則的工程過(guò)程中,這正是1968年NATO軟件工程會(huì)議所提出的目標(biāo).我們可以使用形式化方法討論和說(shuō)明一種軟件開(kāi)發(fā)方法的科學(xué)性以及開(kāi)發(fā)過(guò)程的可信性.在這個(gè)過(guò)程中,形式化可以提高開(kāi)發(fā)的嚴(yán)密性,用抽象和分解手段有效處理復(fù)雜性,尤其是通過(guò)精確描述復(fù)雜系統(tǒng)行為、基于精化的設(shè)計(jì)、將開(kāi)發(fā)過(guò)程制品轉(zhuǎn)換成可以分析驗(yàn)證的規(guī)約等手段,能夠有效地提高在巨大的設(shè)計(jì)空間中逼近最合適設(shè)計(jì)的能力.

2.3.2 程序綜合

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

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

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

還有一些方法允許用戶在程序規(guī)約以外提供代碼框架(或是語(yǔ)法).這樣做有如下兩個(gè)優(yōu)點(diǎn):首先,提供的語(yǔ)法極大地縮小了代碼空間,從而極大地提升了搜索效率;其次,由于程序是按照給定的語(yǔ)法生成的,學(xué)習(xí)到的程序更容易讀懂.SKETCH[152]系統(tǒng)允許用戶提交代碼片段,然后再根據(jù)用戶提交的規(guī)約補(bǔ)全代碼片段.FlashFill[153,154]使用正則表達(dá)式定義了一個(gè)操作字符串的領(lǐng)域?qū)Ｓ谜Z(yǔ)言,然后基于解釋空間(version-space)的代數(shù)來(lái)高效地從輸入輸出對(duì)中獲取對(duì)應(yīng)的程序,在微軟表格中得到了廣泛的應(yīng)用.

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

3 形式驗(yàn)證

形式化方法最顯著的作用是能夠?qū)π问揭?guī)約進(jìn)行驗(yàn)證.形式驗(yàn)證常見(jiàn)的有兩種形式:一種是推理“系統(tǒng)模型規(guī)約是否滿足其性質(zhì)規(guī)約”,這時(shí),模型規(guī)約偏向操作型,性質(zhì)往往是說(shuō)明型的;另一種是推理“系統(tǒng)的一個(gè)模型規(guī)約是否與另一模型規(guī)約有精化或等價(jià)關(guān)系”.這些推理過(guò)程給出了一套靜態(tài)方法來(lái)預(yù)測(cè)系統(tǒng)的行為:用戶可以描述系統(tǒng)行為的所期望性質(zhì)或者開(kāi)發(fā)過(guò)程中不同抽象之間關(guān)系的猜想,形式驗(yàn)證通過(guò)機(jī)械化的方式來(lái)證實(shí)或者證偽這個(gè)性質(zhì)或者猜想,從而提高用戶對(duì)規(guī)約和系統(tǒng)的可信程度.形式驗(yàn)證方法主要包括演繹式的定理證明和算法式的模型檢驗(yàn).

3.1 定理證明

基于定理證明的形式驗(yàn)證將“系統(tǒng)滿足其規(guī)約”這一論斷作為邏輯命題,通過(guò)一組推理規(guī)則,以演繹推理的方式對(duì)該命題開(kāi)展證明.基于定理證明的驗(yàn)證大部分是以程序邏輯為理論基礎(chǔ)的,但是程序邏輯并非唯一的驗(yàn)證方法,例如,我們可以基于程序的操作語(yǔ)義直接表達(dá)程序執(zhí)行的安全性、正確性等各種性質(zhì)并證明相關(guān)定理[58,157].

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

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

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

按照證明方式和自動(dòng)化程度的不同,基于定理證明的驗(yàn)證又可以分為兩類,即基于自動(dòng)定理證明器的自動(dòng)驗(yàn)證和基于人機(jī)交互的半自動(dòng)驗(yàn)證.

3.1.1 基于自動(dòng)定理證明器的自動(dòng)驗(yàn)證

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

使用各種定理證明器和自動(dòng)化程序驗(yàn)證技術(shù),人們已經(jīng)實(shí)現(xiàn)了對(duì)一些相對(duì)實(shí)用的、較大規(guī)模的具體系統(tǒng)的驗(yàn)證.具體工作包括微軟研究院 Hawblitzel等人對(duì)操作系統(tǒng)內(nèi)核、分布式系統(tǒng)等系統(tǒng)的驗(yàn)證[170,171].Hawblitzel等人將源程序翻譯到中間語(yǔ)言 Boogie[172],在 Boogie上開(kāi)展驗(yàn)證,并將生成的驗(yàn)證條件交給 Z3自動(dòng)證明.近年來(lái),類似的工作還包括華盛頓大學(xué)對(duì)操作系統(tǒng)內(nèi)核[173]和文件系統(tǒng)[174]的自動(dòng)驗(yàn)證工作.

基于自動(dòng)定理證明的驗(yàn)證工作的優(yōu)點(diǎn)在于驗(yàn)證的效率較高,不需要人手工寫(xiě)證明.然而,由于自動(dòng)定理證明中很多問(wèn)題是不可判定問(wèn)題,而且各個(gè)定理證明器又有各自的能力限制,因此能夠表達(dá)和證明的性質(zhì)有限.為了能夠?qū)崿F(xiàn)自動(dòng)證明,很多時(shí)候需要對(duì)待證明的性質(zhì)和待驗(yàn)證的代碼本身都進(jìn)行重寫(xiě),甚至為了遷就驗(yàn)證的自動(dòng)化而犧牲待驗(yàn)證的性質(zhì)以及代碼的功能.例如,在對(duì)操作系統(tǒng)內(nèi)核的自動(dòng)化驗(yàn)證工作[173]中,為了實(shí)現(xiàn)“一鍵完成(push button verification)”這一特性,內(nèi)核中帶有循環(huán)語(yǔ)句的代碼都被移到了內(nèi)核外部,從而這部分代碼不再屬于自動(dòng)化驗(yàn)證的目標(biāo).

3.1.2 人機(jī)交互的半自動(dòng)化證明

基于定理證明的另一類驗(yàn)證工作,則不強(qiáng)調(diào)使用計(jì)算機(jī)實(shí)現(xiàn)驗(yàn)證的自動(dòng)化,而是利用計(jì)算機(jī)來(lái)解決證明在計(jì)算機(jī)中的表示問(wèn)題以及自動(dòng)檢查證明的正確性的問(wèn)題,證明的構(gòu)造則由人手工和機(jī)器交互,以半自動(dòng)化的方式完成.很多輔助定理證明工具,如Coq[40]和Isabelle/HOL[45]等,都是針對(duì)這一目的進(jìn)行開(kāi)發(fā)的.這類工具往往是利用類型系統(tǒng)和邏輯之間的 Curry-Howard同構(gòu)關(guān)系[146],將構(gòu)造證明的過(guò)程轉(zhuǎn)化為編寫(xiě)程序的過(guò)程,而證明的正確性檢查也變成了類型檢查問(wèn)題.

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

3.2 模型檢驗(yàn)

定理證明中,形式驗(yàn)證把待證明的性質(zhì)直接作為了一個(gè)數(shù)學(xué)定理來(lái)證明,也稱為演繹式驗(yàn)證.與演繹式相對(duì)應(yīng)的一種方式是模型檢驗(yàn)[175-177].模型檢驗(yàn)分別由Clarke和Emerson、Queille和Sifakis在1980年代初各自獨(dú)立提出[19,176],其基本思想是:檢驗(yàn)一個(gè)結(jié)構(gòu)是否滿足一個(gè)公式要比證明公式在所有結(jié)構(gòu)下均被滿足容易得多,進(jìn)而面向并發(fā)系統(tǒng)創(chuàng)立了在有窮狀態(tài)模型上檢驗(yàn)公式可滿足性的驗(yàn)證新形式[178].

模型檢驗(yàn)通過(guò)自動(dòng)遍歷系統(tǒng)模型的有窮狀態(tài)空間來(lái)檢驗(yàn)系統(tǒng)的語(yǔ)義模型與其性質(zhì)規(guī)約之間的滿足關(guān)系,其基本框架如圖3所示.模型檢驗(yàn)中最常見(jiàn)的是時(shí)序模型檢驗(yàn)或邏輯模型檢驗(yàn),其系統(tǒng)規(guī)約大多是基于模型的規(guī)約,使用操作語(yǔ)義描述系統(tǒng)行為,形式模型使用自動(dòng)機(jī)、標(biāo)記遷移系統(tǒng)等;待檢驗(yàn)的性質(zhì)是用時(shí)序邏輯描述的基于性質(zhì)的規(guī)約.如果系統(tǒng)模型不滿足性質(zhì),模型檢驗(yàn)算法會(huì)給出系統(tǒng)行為不滿足性質(zhì)規(guī)約的反例,用戶可以根據(jù)反例進(jìn)行分析和調(diào)試;如果模型檢驗(yàn)未發(fā)現(xiàn)反例,則系統(tǒng)一定滿足所檢驗(yàn)的性質(zhì).

Fig.3 Framework of model checking圖3 模型檢驗(yàn)框架

3.2.1 基本途徑

模型檢驗(yàn)的核心是有窮狀態(tài)空間上的遍歷策略和算法,主要有顯式方法和隱式方法.顯式方法是通過(guò)狀態(tài)計(jì)算來(lái)遍歷狀態(tài)空間,隱式方法是通過(guò)不動(dòng)點(diǎn)計(jì)算來(lái)遍歷狀態(tài)空間.兩者的本質(zhì)都是有窮狀態(tài)空間的窮盡搜索.因而,模型檢驗(yàn)的關(guān)鍵問(wèn)題就是如何應(yīng)對(duì)系統(tǒng)狀態(tài)爆炸,在可表示的狀態(tài)空間和有效的時(shí)間內(nèi)完成搜索.對(duì)于這個(gè)問(wèn)題,主要有3類途徑[179].

(1) 結(jié)構(gòu)化方法:利用定義系統(tǒng)的語(yǔ)法表達(dá)(模型)結(jié)構(gòu)來(lái)緩解狀態(tài)空間爆炸問(wèn)題,典型的方法有對(duì)稱模型檢驗(yàn)[180-182]、On-the-fly的狀態(tài)空間搜索[183,184]、偏序模型檢驗(yàn)[185-187]、參數(shù)化模型檢驗(yàn)[188,189]等等;

(2) 符號(hào)化方法:將模型的遷移結(jié)構(gòu)的狀態(tài)和遷移編碼為邏輯公式,這種符號(hào)化編碼能夠有效壓縮表示狀態(tài)集合的數(shù)據(jù)結(jié)構(gòu),狀態(tài)變遷的操作也相應(yīng)高效.符號(hào)化的編碼方法常?；贐DD[190]、命題公式[191]或者無(wú)量詞的一階約束[192]等等;

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

模型檢驗(yàn)的其他途徑還包括基于自動(dòng)機(jī)理論的模型檢驗(yàn),Vardi和Wolper提出可以基于ω-自動(dòng)機(jī)來(lái)進(jìn)行自動(dòng)驗(yàn)證[184].時(shí)序邏輯模型檢驗(yàn)問(wèn)題可以歸結(jié)為基于自動(dòng)機(jī)理論的模型檢驗(yàn).在這個(gè)途徑中,時(shí)序邏輯性質(zhì)自動(dòng)轉(zhuǎn)換為一個(gè)自動(dòng)機(jī),這樣,系統(tǒng)和性質(zhì)都建模為自動(dòng)機(jī),模型檢驗(yàn)問(wèn)題就歸結(jié)為自動(dòng)機(jī)的語(yǔ)言包含、判空等問(wèn)題.SPIN模型檢驗(yàn)工具就是基于這種方法.

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

實(shí)際系統(tǒng)中存在不確定性,這在信息物理融合系統(tǒng)是固有的,例如系統(tǒng)中物理部件的信息感知不穩(wěn)定、傳輸丟失等等.在這些系統(tǒng)模型的描述中,通過(guò)引入概率或者隨機(jī)元素來(lái)表達(dá)系統(tǒng)的不確定性,并在設(shè)計(jì)策略中,通過(guò)容錯(cuò)、容變機(jī)制來(lái)獲得期望的量化性質(zhì).這類系統(tǒng)量化性質(zhì)的模型檢驗(yàn)有兩種途徑.

· 概率模型檢驗(yàn)[201],其在系統(tǒng)(例如標(biāo)記變遷系統(tǒng))中引入概率遷移,采用可描述隨機(jī)行為數(shù)學(xué)結(jié)構(gòu)(例如馬爾可夫鏈)為形式語(yǔ)義,通過(guò)數(shù)值計(jì)算的方式檢驗(yàn)此類系統(tǒng)是否滿足所期望的概率時(shí)序邏輯性質(zhì)(例如,系統(tǒng)在給定時(shí)間內(nèi)完成相應(yīng)功能的概率).典型的概率模型檢驗(yàn)工具有PRISM[202];

· 統(tǒng)計(jì)模型檢驗(yàn)[203,204],其模擬有窮多次的系統(tǒng)執(zhí)行,然后通過(guò)假設(shè)檢驗(yàn)來(lái)推斷這些樣本是否提供了統(tǒng)計(jì)證據(jù)以表明系統(tǒng)滿足或違反性質(zhì).

概率模型檢驗(yàn)的復(fù)雜度高;統(tǒng)計(jì)模型檢驗(yàn)避免了窮盡搜索,但其結(jié)果具有一定的置信區(qū)間.

3.2.2 軟件模型檢驗(yàn)

軟件系統(tǒng)屬于無(wú)窮狀態(tài)系統(tǒng),即使?fàn)顟B(tài)有窮,其狀態(tài)空間規(guī)模也往往遠(yuǎn)超當(dāng)前計(jì)算機(jī)可處理的范圍.在硬件系統(tǒng)模型檢驗(yàn)取得巨大成功的時(shí)候,軟件模型檢驗(yàn)所面臨的挑戰(zhàn)依然嚴(yán)峻.對(duì)于無(wú)窮狀態(tài)系統(tǒng),符號(hào)化可達(dá)性分析都可能不終止.軟件模型檢驗(yàn)的核心問(wèn)題是如何建立規(guī)模可檢驗(yàn)的軟件模型(抽象).給定軟件S及待驗(yàn)證的性質(zhì)p,抽象模型檢驗(yàn)就是建立一個(gè)抽象映射α,并建立S?p(即S滿足性質(zhì)p)和α(S)?p的關(guān)系.若S?α(S),則稱α(S)為S的上近似(over-approximation);如果α(S)?S,則稱α(S)為S的下近似(under-approximation).

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

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

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

在軟件模型檢驗(yàn)中,利用靜態(tài)分析、符號(hào)執(zhí)行等方法抽取程序模型,以及基于路徑的模型檢驗(yàn)等靜態(tài)和動(dòng)態(tài)結(jié)合的方法,也是有效提高模型檢驗(yàn)擴(kuò)展性的重要途徑[3].近年來(lái),將模型檢驗(yàn)與定理證明有效地結(jié)合也是一個(gè)有前景的方向.

4 形式化方法的應(yīng)用

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

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

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

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

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

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

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

5 形式化方法面臨的挑戰(zhàn)與未來(lái)

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

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

近 10年來(lái),形式化方法進(jìn)入一個(gè)振興的階段.無(wú)論是輕量級(jí)的形式化方法與主流方法的結(jié)合,還是重量級(jí)的形式化方法在工業(yè)級(jí)軟件上的應(yīng)用,都取得了較大的進(jìn)步和成功[237].在這些成功應(yīng)用的后面,工具起到了決定性的作用.系統(tǒng)一旦使用了形式規(guī)約語(yǔ)言建模,它就能用工具進(jìn)行語(yǔ)義分析.工具也緩解了問(wèn)題規(guī)模帶來(lái)的壓力.因此,構(gòu)建更加可用和魯棒的工具支持大規(guī)模規(guī)約的并行語(yǔ)義分析和驗(yàn)證,構(gòu)建可復(fù)用的形式規(guī)約庫(kù)和方法社區(qū),推動(dòng)形式化方法工具和可復(fù)用庫(kù)設(shè)施的進(jìn)步,包括工具的集成、工具的無(wú)形化、規(guī)約與驗(yàn)證資產(chǎn),毫無(wú)疑問(wèn)都會(huì)是形式化方法努力的方向.

規(guī)約、開(kāi)發(fā)和驗(yàn)證的系統(tǒng)與環(huán)境的形態(tài)變化是形式化方法發(fā)展的驅(qū)動(dòng)力.形式化方法的目標(biāo)在于高質(zhì)量的描述、開(kāi)發(fā)和確認(rèn)軟件系統(tǒng),因而軟/硬件的形態(tài)進(jìn)步和地位的變化對(duì)形式化方法有著直接的影響.例如,形式化方法發(fā)展的一條重要線索是從順序程序到并行程序、混成系統(tǒng)、信息物理融合系統(tǒng)乃至人機(jī)物融合系統(tǒng),而人機(jī)物融合社會(huì)中混成系統(tǒng)對(duì)形式化方法的基礎(chǔ)、方法、技術(shù)和工具都形成了全面的挑戰(zhàn)[238,239].

軟件正在成為社會(huì)基礎(chǔ)設(shè)施,而形式化方法在計(jì)算機(jī)系統(tǒng)基礎(chǔ)軟/硬件的可靠性中發(fā)揮了十分重要的作用,這正是人們最能認(rèn)識(shí)到的形式化方法在關(guān)鍵的信息基礎(chǔ)設(shè)施中發(fā)揮作用的應(yīng)用點(diǎn).在軟件基礎(chǔ)設(shè)施方面,全棧的可驗(yàn)證軟件將會(huì)持續(xù)地進(jìn)展,并有可能在實(shí)用主流操作系統(tǒng)中逐漸地滲透.例如,為了保證云服務(wù)基礎(chǔ)設(shè)施的可靠性,Amazon利用TLA+方法對(duì)其S3云存儲(chǔ)服務(wù)的關(guān)鍵算法進(jìn)行了形式驗(yàn)證,發(fā)現(xiàn)了不少缺陷[240].2017年,Linux基金會(huì)宣稱,將對(duì)一些 Linux內(nèi)核模塊進(jìn)行形式驗(yàn)證以提高系統(tǒng)的安全性[241].基于形式化方法的信息安全性研究毫無(wú)疑問(wèn)是一個(gè)方向[242].面向未來(lái)的軟件基礎(chǔ)設(shè)施,區(qū)塊鏈和智能合約的正確性及信息安全性驗(yàn)證正蓬勃展開(kāi)[243,244].

在軟件定義一切的時(shí)代,形式化方法將定義軟件.形式化方法如何與其他軟件開(kāi)發(fā)方法、領(lǐng)域特定的融合顯得尤為重要.對(duì)應(yīng)于軟件定義時(shí)代的軟件形態(tài)的特征變化、質(zhì)量的需求變化,形式化方法需要在基礎(chǔ)概念、規(guī)約、開(kāi)發(fā)和驗(yàn)證技術(shù)與工具上適應(yīng)更為復(fù)雜開(kāi)放、動(dòng)態(tài)多變、持續(xù)演化的軟件形態(tài).例如,在人機(jī)物融合下,需要準(zhǔn)確、恰當(dāng)?shù)靥幚矸切问交枨蟮叫问揭?guī)約、形式化抽象到非形式化場(chǎng)景和現(xiàn)實(shí)世界的邊界建模,大量非功能規(guī)約包括社會(huì)化人因的規(guī)約,自主自適應(yīng)自組織等新型軟件結(jié)構(gòu)和行為的規(guī)約、推理與驗(yàn)證等等.在形式化方法的發(fā)展中,數(shù)學(xué)與形式化方法有著密切的互動(dòng),數(shù)學(xué)為形式化模型和推理提供了基礎(chǔ),而形式化方法也促進(jìn)了數(shù)學(xué)的發(fā)展.形式化方法可以機(jī)械、高效、準(zhǔn)確無(wú)誤地寫(xiě)出復(fù)雜數(shù)學(xué)問(wèn)題的可靠證明,甚至幫助解決一些長(zhǎng)期懸而未決的數(shù)學(xué)難題,例如四色定理[245]、羅賓斯猜想(Robbins conjecture)[246]、開(kāi)普勒猜想(Kepler conjecture)[247](該原始證明超過(guò) 300多頁(yè),正式發(fā)表的證明也近 130頁(yè),其正確性無(wú)法保證[248])等等.形式化(工程)數(shù)學(xué)[249]對(duì)于構(gòu)建高可信智能制造軟件環(huán)境也具有重要價(jià)值.

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

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

計(jì)算思維的滲透性也帶動(dòng)了形式化方法與其他學(xué)科的交叉融合,例如在生物研究領(lǐng)域,計(jì)算建模和分析已經(jīng)成為一種重要方法[253],例如Na?ve T cell differentiation的時(shí)序行為建模和分析[254].這些研究有力地促進(jìn)了混成系統(tǒng)形式化方法的發(fā)展,也促進(jìn)了醫(yī)療生命科學(xué)的發(fā)展,并為醫(yī)工結(jié)合交叉提供了一個(gè)明確的方向[255].

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

6 結(jié)束語(yǔ)

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

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