面向計(jì)算機(jī)并發(fā)程序的形式化驗(yàn)證方法設(shè)計(jì)*

謝小賦，曾夢(mèng)岐，龐 飛

（中國電子科技集團(tuán)有限公司第三十研究所，四川 成都 610041）

0 引 言

形式化驗(yàn)證作為一種基于嚴(yán)格數(shù)學(xué)推理的計(jì)算機(jī)軟件安全性和可靠性保障技術(shù)，近年來已經(jīng)取得了巨大的進(jìn)展。但是，隨著計(jì)算機(jī)系統(tǒng)越來越復(fù)雜，提供的功能越來越強(qiáng)大，其蘊(yùn)含的安全性問題也日益嚴(yán)峻，因此對(duì)形式化驗(yàn)證方法提出了更高的要求。計(jì)算機(jī)并發(fā)技術(shù)在高效利用計(jì)算機(jī)資源的同時(shí)，可能存在對(duì)計(jì)算機(jī)軟件安全造成很大威脅的并發(fā)錯(cuò)誤。利用形式化驗(yàn)證找出軟件中的并發(fā)錯(cuò)誤并排除其帶來的安全隱患成為形式化方法研究領(lǐng)域的一個(gè)重點(diǎn)方向。

基于形式化驗(yàn)證并發(fā)錯(cuò)誤的研究主要包含兩個(gè)方面：以定理證明為例的演繹推理方法和以模型檢測(cè)為例的建模和驗(yàn)證方法[1]。前者通常利用從系統(tǒng)生成的一組規(guī)則并進(jìn)行推理證明，以驗(yàn)證系統(tǒng)是否滿足指定的規(guī)則。而模型檢測(cè)是一種對(duì)有限狀態(tài)的并發(fā)軟件系統(tǒng)進(jìn)行自動(dòng)化驗(yàn)證的技術(shù)[2]，其實(shí)現(xiàn)方式是使用過程建模語言將需要驗(yàn)證的軟件系統(tǒng)進(jìn)行重新建模，將軟件系統(tǒng)內(nèi)部的數(shù)據(jù)、行為和實(shí)體進(jìn)行抽象，并在系統(tǒng)模型代碼中加入相應(yīng)的并發(fā)性驗(yàn)證代碼，最后輸入到模型檢查引擎中得出并發(fā)性驗(yàn)證結(jié)果。

經(jīng)過相關(guān)工作人員的大量研究，目前針對(duì)并發(fā)程序的形式化驗(yàn)證工作已經(jīng)有部分成效。在早期的研究中，Taylor[3]給出并發(fā)狀態(tài)、并發(fā)歷史等相關(guān)概念，并且提出了一種基于并發(fā)歷史的并發(fā)錯(cuò)誤分析方法。Foster等人[4]將定理證明這一形式化方法引入并發(fā)問題檢測(cè)中，通過對(duì)程序的形式化規(guī)約進(jìn)行靜態(tài)分析以檢測(cè)并發(fā)性漏洞。Enans[5]在工具LCLint中實(shí)現(xiàn)了靜態(tài)檢測(cè)方法，并通過內(nèi)存標(biāo)注來檢測(cè)并發(fā)錯(cuò)誤。在并發(fā)性形式化驗(yàn)證的早期研究中，檢測(cè)目標(biāo)的規(guī)模一般較小，復(fù)雜度不高，驗(yàn)證過程的自動(dòng)化程度較低，難以驗(yàn)證大型并發(fā)軟件。

在近年針對(duì)軟件并發(fā)性驗(yàn)證的研究中，研究人員基于驗(yàn)證對(duì)象提出了不同的框架和方法。例如，采用符號(hào)執(zhí)行、進(jìn)程代數(shù)分析以及模型檢測(cè)等方式和思路，對(duì)軟件的并發(fā)性進(jìn)行了形式化驗(yàn)證。相較于早期的研究，其在自動(dòng)化程度上有了進(jìn)一步的提升。Kaki等人[6]利用進(jìn)程代數(shù)，提出了一種針對(duì)并發(fā)和分布式程序行為特性的驗(yàn)證技術(shù)，這種技術(shù)使用進(jìn)程代數(shù)對(duì)建模程序行為進(jìn)行自動(dòng)抽象，彌補(bǔ)了程序?qū)崿F(xiàn)與其模型之間的典型差距。吳亞楠[7]設(shè)計(jì)了一個(gè)動(dòng)態(tài)數(shù)據(jù)競(jìng)爭(zhēng)檢測(cè)工具，提出了一種分層過濾的方法，可以減少動(dòng)態(tài)監(jiān)視程序執(zhí)行行為的高性能開銷，以實(shí)現(xiàn)高效檢測(cè)多線程程序的數(shù)據(jù)競(jìng)爭(zhēng)和驗(yàn)證有害競(jìng)爭(zhēng)。Foster等人[8]提出了一種具有大或無限狀態(tài)空間的并行反應(yīng)程序的代數(shù)驗(yàn)證策略，并利用反應(yīng)關(guān)系和克萊尼代數(shù)證明了該策略的可行性。進(jìn)程代數(shù)分析和符號(hào)執(zhí)行的引入使得并發(fā)系統(tǒng)定義的精確程度有了進(jìn)一步的提高，但在驗(yàn)證效率方面依然無法支持大型復(fù)雜軟件的并發(fā)性驗(yàn)證工作。

隨著形式化方法中模型檢測(cè)技術(shù)的發(fā)展和完善，不斷有研究人員將其應(yīng)用在并發(fā)性形式化驗(yàn)證上。Guellati等人[9]改進(jìn)了自動(dòng)狀態(tài)機(jī)的模型檢測(cè)算法，將基于時(shí)間計(jì)算樹邏輯（Time Computation Tree Logic，TCTL）模型檢查算法應(yīng)用于持續(xù)動(dòng)作定時(shí)自動(dòng)機(jī)模型，對(duì)模型檢驗(yàn)算法和可表達(dá)及驗(yàn)證的性質(zhì)范圍進(jìn)行了改進(jìn)和擴(kuò)展，使得模型可以捕捉系統(tǒng)行為中真正的并發(fā)性。David等人[10]研究了一套基于依賴保證的并發(fā)程序驗(yàn)證框架（CSim2），可實(shí)現(xiàn)對(duì)并發(fā)系統(tǒng)進(jìn)行自頂向下的組合驗(yàn)證，通過使用模擬框架，在頂層上進(jìn)行驗(yàn)證的屬性被組合傳播到系統(tǒng)每個(gè)并發(fā)組件中的最低源碼層。

目前針對(duì)系統(tǒng)并發(fā)性形式化驗(yàn)證的研究在許多層面已有突破，但仍存在一些難點(diǎn)和問題。首先，推理低效困難，普通驗(yàn)證過程通常采用單一的源碼或者字節(jié)碼進(jìn)行底層驗(yàn)證，并發(fā)性驗(yàn)證需要證明高層的安全屬性，如死鎖、可達(dá)性、無散度判別等。而源碼級(jí)別涉及太多的無意義變量與邏輯，導(dǎo)致驗(yàn)證效率很差。其次，驗(yàn)證系統(tǒng)存在模型間的語義鴻溝，功能驗(yàn)證和行為驗(yàn)證所用的方法不同，缺乏抽象端到源碼端的一致性證明。

針對(duì)計(jì)算機(jī)軟件并發(fā)性驗(yàn)證的難點(diǎn)，本文提出了一種可雙向轉(zhuǎn)換的并發(fā)性形式化驗(yàn)證方法，解決了普通抽象過程中建模驗(yàn)證缺乏靈活性的問題，避免了對(duì)系統(tǒng)進(jìn)行重復(fù)抽象建模，并且保證了源碼層與抽象層驗(yàn)證的一致性。文章首先介紹了驗(yàn)證方法的基本路線，路線分別從代碼功能正確性和行為功能正確性兩方面進(jìn)行程序的驗(yàn)證，以保證最終的驗(yàn)證一致性。其次對(duì)框架的整體設(shè)計(jì)思路進(jìn)行了詳盡的描述，方法根據(jù)輸入的源碼應(yīng)用程序接口（Application Programming Interface，API）與功能需求文檔，通過模型規(guī)范提取器和形式化命題生成器抽取規(guī)范表示并輸入到中間映射層，自動(dòng)向上映射生成相應(yīng)的通信順序進(jìn)程（Communication Sequential Process，CSP）模型，向下映射生成相應(yīng)的功能性規(guī)范。經(jīng)過自動(dòng)驗(yàn)證器完成并發(fā)性驗(yàn)證和功能性驗(yàn)證。最后基于該并發(fā)性驗(yàn)證方法進(jìn)行應(yīng)用案例分析。

1 并發(fā)性驗(yàn)證基本路線

以CSP過程建模為例的并發(fā)性形式化驗(yàn)證方法使用模型檢查技術(shù)，通過系統(tǒng)抽象獲取整體模型，利用自動(dòng)化驗(yàn)證器完成并發(fā)性驗(yàn)證。為保證系統(tǒng)整體的安全性，還需要對(duì)計(jì)算機(jī)軟件的功能正確性進(jìn)行驗(yàn)證，但是因?yàn)橄到y(tǒng)中存在模型間的語義鴻溝，無法保證并發(fā)性驗(yàn)證模型和功能正確性驗(yàn)證模型的一致性。如果交由人工編寫功能規(guī)范再進(jìn)行復(fù)雜的一致性推理，則會(huì)嚴(yán)重影響驗(yàn)證效率。為此，本文提出了一種可以保證源碼端和抽象端一致性的可雙向轉(zhuǎn)換的并發(fā)性驗(yàn)證方法。方法路線如圖1所示。

基于輸入的源碼API及其用自然語言給出的功能規(guī)范，路線分為代碼端的功能正確性驗(yàn)證和抽象端的行為并發(fā)性驗(yàn)證。

整體的驗(yàn)證路線為首先根據(jù)提供的函數(shù)API以及需求規(guī)范說明文檔進(jìn)行規(guī)范提取，然后轉(zhuǎn)化為一種抽象度居中的中間層規(guī)范。這種中間層規(guī)范既可以自動(dòng)向上映射為高層規(guī)范并輸入到并發(fā)性驗(yàn)證模塊中進(jìn)行并發(fā)屬性驗(yàn)證，也可以自動(dòng)向下映射為源碼層規(guī)范并輸入到功能性驗(yàn)證模塊中進(jìn)行功能正確性驗(yàn)證，經(jīng)過兩條路線驗(yàn)證后，最終得到驗(yàn)證結(jié)果。整體的驗(yàn)證步驟如圖2所示。

中間層規(guī)范是指對(duì)源碼規(guī)范與需求進(jìn)行了適度抽象的形式化表示。一方面，中間層規(guī)范不僅完整地描述了底層程序功能，而且過濾了程序?qū)崿F(xiàn)細(xì)節(jié)，使得程序安全驗(yàn)證可同時(shí)映射高層與底層兩個(gè)方向，解決了高層抽象驗(yàn)證與源碼級(jí)驗(yàn)證之間存在的語義鴻溝，提供了高層屬性端到源碼端的一致性驗(yàn)證。另一方面，生成中間層規(guī)范時(shí)可以一次性覆蓋所有源碼API，從中間層規(guī)范自動(dòng)向上映射出過程模型分析系統(tǒng)并發(fā)屬性，避免了對(duì)整個(gè)系統(tǒng)進(jìn)行人工的重復(fù)建模，提高了系統(tǒng)靈活性。

2 并發(fā)性驗(yàn)證方法設(shè)計(jì)

可雙向轉(zhuǎn)換的并發(fā)性驗(yàn)證方法設(shè)計(jì)架構(gòu)整體可分為中間層規(guī)范生成模塊、自動(dòng)化功能性驗(yàn)證模塊、自動(dòng)化并發(fā)性驗(yàn)證模塊以及集成模塊。其中，中間層規(guī)范生成模塊主要用于將源碼API信息與文檔功能需求整合并生成一種可以雙分支映射的中間層規(guī)范；自動(dòng)化功能性驗(yàn)證模塊主要通過自動(dòng)向下映射機(jī)制使中間層規(guī)范轉(zhuǎn)化為源碼級(jí)驗(yàn)證模型，再通過自動(dòng)化功能性驗(yàn)證工具進(jìn)行功能性驗(yàn)證，并得出功能正確性驗(yàn)證結(jié)果；自動(dòng)化并發(fā)性驗(yàn)證模塊主要通過自動(dòng)向上映射機(jī)制使中間層規(guī)范轉(zhuǎn)換為抽象過程模型，再通過自動(dòng)化并發(fā)性驗(yàn)證工具進(jìn)行并發(fā)屬性驗(yàn)證，得到并發(fā)性驗(yàn)證結(jié)果；集成模塊根據(jù)并發(fā)屬性驗(yàn)證與功能性驗(yàn)證的結(jié)果，最終生成具有跨模型邏輯一致性的安全驗(yàn)證結(jié)果。

2.1 中間層規(guī)范生成模塊設(shè)計(jì)

中間層規(guī)范模塊由形式化命題生成器、模型規(guī)范提取器和中間層規(guī)范生成器組成。模塊結(jié)構(gòu)設(shè)計(jì)如圖3所示。

形式化命題生成器用于對(duì)輸入的源碼進(jìn)行形式化表示，通過分析待驗(yàn)證程序中所有的變量，將其作為所述中間層規(guī)范中的行為載體；確定待驗(yàn)證程序中的主要狀態(tài)變遷依靠的函數(shù)，將其設(shè)置為功能元素；隱藏底層內(nèi)存狀態(tài)，引入等價(jià)的抽象狀態(tài)用于表述底層完整功能邏輯，忽略函數(shù)變量具體的取值，只考慮相應(yīng)的狀態(tài)變遷及變遷條件，并描述出函數(shù)具體內(nèi)部邏輯。模型規(guī)范提取器根據(jù)提供的代碼流程以及相應(yīng)的需求說明文檔，將文檔中關(guān)于代碼的邏輯限制轉(zhuǎn)化為便于進(jìn)行形式化描述的模型規(guī)范。獲得的模型規(guī)范為一種抽象度居中的形式化描述，用于輸入到中間層規(guī)范生成器中。中間層規(guī)范生成器根據(jù)輸入的形式化命題與相應(yīng)的模型規(guī)范，整合成為一種抽象度居中的中間層規(guī)范。從整體而言，中間層規(guī)范模塊一次性處理所有的API，轉(zhuǎn)化為所述中間層規(guī)范。

將中間層規(guī)范輸入到自動(dòng)化功能性驗(yàn)證模塊與自動(dòng)化并發(fā)性驗(yàn)證模塊，即可進(jìn)行自動(dòng)化驗(yàn)證和并發(fā)性驗(yàn)證。

2.2 自動(dòng)化并發(fā)性驗(yàn)證模塊設(shè)計(jì)

自動(dòng)化并發(fā)驗(yàn)證模塊主要負(fù)責(zé)提供抽象端的并發(fā)性驗(yàn)證，通過雙向轉(zhuǎn)換器將中間層規(guī)范自動(dòng)向上映射為抽象層規(guī)范。其完成并發(fā)性驗(yàn)證的具體步驟描述如下：

步驟1：根據(jù)所述中間層規(guī)范表現(xiàn)出的狀態(tài)間邏輯關(guān)系進(jìn)行抽象；

步驟2：確定狀態(tài)間轉(zhuǎn)移條件，形成不同的抽象路徑，每條路徑包含相應(yīng)的前置后置狀態(tài)；

步驟3：對(duì)所述中間層規(guī)范進(jìn)行分析，確定路徑相關(guān)性，將并發(fā)的路徑并列起來，生成相應(yīng)的高層規(guī)范；

步驟4：根據(jù)高層規(guī)范得到高層抽象狀態(tài)機(jī)，并參考系統(tǒng)的狀態(tài)遷移屬性，推理出狀態(tài)遷移合法性規(guī)則，編寫高層屬性規(guī)范；

步驟5：依據(jù)所述高層抽象狀態(tài)機(jī)中的狀態(tài)、行為及邏輯信息，形成可用于并發(fā)推理的抽象過程模型，再根據(jù)所述高層規(guī)范與所述高層屬性規(guī)范，生成并插入并發(fā)安全屬性語句，最后進(jìn)行并發(fā)屬性驗(yàn)證。

2.3 自動(dòng)化功能性驗(yàn)證模塊設(shè)計(jì)

自動(dòng)化功能性驗(yàn)證模塊主要負(fù)責(zé)提供源碼級(jí)的功能正確性驗(yàn)證，在生成可雙向映射的中間層規(guī)范后，經(jīng)由雙向轉(zhuǎn)換器自動(dòng)向下映射為源碼級(jí)規(guī)范，經(jīng)過細(xì)節(jié)抽取、驗(yàn)證函數(shù)生成、規(guī)范生成和最終驗(yàn)證4個(gè)步驟完成功能性驗(yàn)證。關(guān)鍵步驟描述如下：

步驟1：根據(jù)所述中間層規(guī)范給出的函數(shù)調(diào)用關(guān)系，抽取函數(shù)實(shí)現(xiàn)邏輯以及函數(shù)內(nèi)部變量的數(shù)據(jù)結(jié)構(gòu)和傳遞條件；

步驟2：根據(jù)所述數(shù)據(jù)結(jié)構(gòu)和傳遞條件，分析函數(shù)應(yīng)達(dá)到的安全標(biāo)準(zhǔn)，將其生成為一個(gè)源碼級(jí)形式化規(guī)范；

步驟3：將生成的所述源碼級(jí)形式化規(guī)范插入到源碼中，形成源碼級(jí)驗(yàn)證模型；

步驟4：將轉(zhuǎn)換輸出的所述源碼級(jí)驗(yàn)證模型進(jìn)行功能性驗(yàn)證。系統(tǒng)整體的工作流程圖如圖4所示。

2.4 集成模塊設(shè)計(jì)

集成模塊由結(jié)果生成器組成。結(jié)果生成器根據(jù)中間層規(guī)范模塊中的并發(fā)屬性驗(yàn)證與功能性驗(yàn)證情況，生成具有跨模型邏輯一致性的安全驗(yàn)證結(jié)果。

集合模塊整合了屬性并發(fā)性和功能正確性的驗(yàn)證結(jié)果，最后生成一份源碼安全性報(bào)告。

3 實(shí)驗(yàn)過程和結(jié)果

本文以一個(gè)C語言實(shí)現(xiàn)的融資程序?yàn)榘咐?，采用第二?jié)所述的雙向并發(fā)性驗(yàn)證方法對(duì)程序進(jìn)行驗(yàn)證：

案例程序主要的功能為控制融資金額，預(yù)先給定一個(gè)最低融資目標(biāo)，當(dāng)實(shí)際融資金額小于融資目標(biāo)時(shí)，可以進(jìn)行相應(yīng)的融資操作；當(dāng)融資金額大于或等于相應(yīng)的融資目標(biāo)時(shí)，更新融資狀態(tài)為關(guān)閉狀態(tài)。此案例涉及金融安全領(lǐng)域，對(duì)代碼安全性要求較高，因此需要采用形式化驗(yàn)證方法使程序滿足相應(yīng)的安全性需求。本文將對(duì)該程序生成抽象度居中的中間層規(guī)范，再進(jìn)行雙向自動(dòng)化映射以及驗(yàn)證器驗(yàn)證，最后根據(jù)結(jié)果分析說明本文所述方法的有效性。

3.1 中間層規(guī)范生成

步驟1：首先對(duì)于案例程序來說，確定聲明中g(shù)oal與raised為函數(shù)變量，在中間層規(guī)范中體現(xiàn)為實(shí)際的行為載體；再確定程序內(nèi)部狀態(tài)變遷的主要邏輯依靠invest函數(shù)內(nèi)部行為來實(shí)現(xiàn)，則將invest定義為中間層規(guī)范中的FUNCTION元素。

步驟2：函數(shù)內(nèi)部邏輯為當(dāng)融資金額小于目標(biāo)時(shí)，進(jìn)行融資操作；考慮到中間層規(guī)范既要隱藏底層具體繁雜的內(nèi)存狀態(tài)，又要引入等價(jià)的抽象狀態(tài)用于表述底層完整功能邏輯，raised涉及兩種狀態(tài)，則將其聲明為一個(gè)old(raised)帶有時(shí)間性質(zhì)的元素類型，當(dāng)old(raised)

步驟3：根據(jù)上述操作，將程序中所有API都整合為中間層規(guī)范；本例中invest整合出的中間層規(guī)范為：

3.2 自動(dòng)向上映射及并發(fā)屬性驗(yàn)證

步驟1：根據(jù)中間層規(guī)范中表現(xiàn)出的狀態(tài)間邏輯關(guān)系進(jìn)行抽象。

步驟2：確定每個(gè)狀態(tài)之間的轉(zhuǎn)移條件，形成不同的抽象路徑，每條路徑包含相應(yīng)的前置后置狀態(tài)。對(duì)于本例來說，中間層規(guī)范中的invest函數(shù)抽象出的路徑為兩條，以第一條路徑為例，前置條件為(raised

步驟3：對(duì)完整的中間層規(guī)范進(jìn)行分析，確定每一條路徑的相關(guān)性，將可并發(fā)產(chǎn)生的路徑并列起來；經(jīng)過對(duì)所有路徑的分析，得到的invest高層規(guī)范代碼為：

步驟4：根據(jù)高層規(guī)范得到invest函數(shù)高層抽象狀態(tài)機(jī)，參考整個(gè)系統(tǒng)的狀態(tài)遷移屬性，推理出狀態(tài)遷移合法性規(guī)則，編寫高層屬性規(guī)范。在本例中，參考invest函數(shù)路徑，考慮到一旦募集成功，融資金額不能低于最低融資目標(biāo)，則本例得到的高層屬性規(guī)范代碼為：

步驟5：根據(jù)高層規(guī)范，生成相應(yīng)的CSP模型代碼；根據(jù)相應(yīng)的高層屬性規(guī)范及系統(tǒng)需求文檔給出的并發(fā)性要求，編寫相應(yīng)的并發(fā)屬性判 斷 語 句，如：#assert P() deadlock，#assert P()deterministic等；并將判斷語句插入到CSP抽象過程模型代碼中，最后輸入到自動(dòng)化并發(fā)驗(yàn)證模塊進(jìn)行系統(tǒng)并發(fā)模擬驗(yàn)證，并得出并發(fā)性驗(yàn)證結(jié)果。

3.3 自動(dòng)向下映射及功能性驗(yàn)證

步驟1：根據(jù)中間層規(guī)范給出的函數(shù)調(diào)用關(guān)系，抽取具體的函數(shù)實(shí)現(xiàn)邏輯，以及函數(shù)內(nèi)部變量的數(shù)據(jù)傳遞結(jié)構(gòu)和傳遞條件。

步驟2：根據(jù)具體的數(shù)據(jù)傳遞結(jié)構(gòu)及條件，自動(dòng)化分析函數(shù)模塊應(yīng)該達(dá)到的安全標(biāo)準(zhǔn)，將其生成為一個(gè)單獨(dú)的驗(yàn)證函數(shù)。在本例中，參考中間層規(guī)范中表述當(dāng)raised舊值小于最低目標(biāo)融資時(shí)，函數(shù)會(huì)進(jìn)行融資操作，自動(dòng)生成一條判斷函數(shù)語句：assert(raised == old_raised + value)。

步驟3：將自動(dòng)生成的單獨(dú)驗(yàn)證函數(shù)插入到源碼中，形成最后輸出的源碼級(jí)規(guī)范，本例生成代碼為：

步驟4：將生成的源碼級(jí)規(guī)范輸入到功能性驗(yàn)證工具中，根據(jù)規(guī)范中單獨(dú)的驗(yàn)證函數(shù)為功能性驗(yàn)證工具調(diào)整參數(shù)，使其可以完全覆蓋函數(shù)本身的邏輯分支，并得出功能性驗(yàn)證結(jié)果。

3.4 驗(yàn)證結(jié)果分析

上述案例首先通過代碼邏輯信息及功能需求整合出了相應(yīng)的中間層規(guī)范，描述了行為載體goal，raised，state與功能元素invest，close之間的邏輯關(guān)系。一方面，通過自動(dòng)向上映射生成了高層規(guī)范，根據(jù)invest元素的功能邏輯編寫了高層屬性規(guī)范，最終插入相應(yīng)并發(fā)性斷言進(jìn)行了自動(dòng)化并發(fā)性驗(yàn)證。另一方面，通過自動(dòng)向下映射生成了相應(yīng)的源碼級(jí)規(guī)范，根據(jù)raised行為載體的邏輯需求插入了功能性斷言并進(jìn)行了自動(dòng)化功能性驗(yàn)證。

在本例中，自動(dòng)化并發(fā)性驗(yàn)證模塊與功能性驗(yàn)證模塊給出的驗(yàn)證結(jié)果均為正確，表示驗(yàn)證過程中生成規(guī)范與斷言均得到了滿足，源碼層的功能性規(guī)范與抽象層的并發(fā)屬性規(guī)范通過了驗(yàn)證。驗(yàn)證結(jié)果表明，本例設(shè)計(jì)的形式化驗(yàn)證方法成功證明了融資程序的源碼級(jí)實(shí)現(xiàn)與相應(yīng)抽象層屬性之間的邏輯一致性。

在驗(yàn)證流程中，一方面，通過中間層規(guī)范雙向映射的驗(yàn)證方法，消除了高層抽象驗(yàn)證與源碼級(jí)驗(yàn)證的語義鴻溝。另一方面，生成中間層規(guī)范時(shí)一次性覆蓋了所有源碼API，避免了對(duì)系統(tǒng)進(jìn)行人工重復(fù)建模。在實(shí)際驗(yàn)證流程中，雙向映射過程采用自動(dòng)化工具完成，相較于傳統(tǒng)并發(fā)程序驗(yàn)證采用的手動(dòng)驗(yàn)證方式，降低了人工參與度，提高了驗(yàn)證效率。

4 結(jié) 語

本文以C語言程序源碼的并發(fā)性驗(yàn)證方法為研究對(duì)象，提出了一種可雙向轉(zhuǎn)換的并發(fā)性驗(yàn)證方法，針對(duì)傳統(tǒng)并發(fā)性驗(yàn)證建模缺乏靈活性的問題進(jìn)行了改進(jìn)，并在整個(gè)驗(yàn)證過程中提供了從抽象端到源碼端的一致性保證。首先，根據(jù)可雙向轉(zhuǎn)換的并發(fā)驗(yàn)證思路設(shè)計(jì)了驗(yàn)證系統(tǒng)的框架；其次，根據(jù)整體驗(yàn)證思路設(shè)計(jì)了一種中間層規(guī)范生成器，將提供的代碼及需求說明文檔轉(zhuǎn)化為中間層規(guī)范；最后，設(shè)計(jì)了一種自動(dòng)化雙向轉(zhuǎn)換器，將中間層規(guī)范自動(dòng)映射為高層規(guī)范與功能性規(guī)范并分別進(jìn)行驗(yàn)證。根據(jù)對(duì)融資程序的試驗(yàn)驗(yàn)證，證明了此雙向轉(zhuǎn)換并發(fā)性驗(yàn)證方法的有效性及可用性。未來主要是在面向更復(fù)雜的驗(yàn)證目標(biāo)時(shí)能更好地提供效率保障，并且在實(shí)際的驗(yàn)證工作中提高自動(dòng)化程度，減少人工參與度。