當(dāng)今世界是一個(gè)軟件定義一切的時(shí)代,尤其在安全攸關(guān)領(lǐng)域,需要保證計(jì)算機(jī)程序的可靠運(yùn)行。這種可靠性可以通過向程序傳遞所有可能的測(cè)試用例的方法來實(shí)現(xiàn),但該方法難以保證一些輸入范圍無限的復(fù)雜程序的正確性。形式驗(yàn)證的目的是構(gòu)建程序正確性的數(shù)學(xué)說明,但所需驗(yàn)證工作是繁瑣的,而且容易出錯(cuò),使用自動(dòng)驗(yàn)證工具使證明過程自動(dòng)化是目前形式驗(yàn)證的一種趨勢(shì)。Dafny是微軟研究院創(chuàng)建的一種內(nèi)置規(guī)約結(jié)構(gòu)的編程語言和靜態(tài)程序證明器,其目的是驗(yàn)證程序的功能正確性并可將程序驗(yàn)證過程完全自動(dòng)化。這大大減少了繁瑣的程序驗(yàn)證過程,極大提高了軟件的可靠性。必須認(rèn)識(shí)到,現(xiàn)階段Dafny程序的生成沒有特定的方法和工具,很多問題的Dafny程序都是基于開發(fā)者的經(jīng)驗(yàn),而且Dafny程序中循環(huán)不變式都是從天而降的,基于開發(fā)者對(duì)算法設(shè)計(jì)的熟練程度。本文結(jié)合算法程序設(shè)計(jì)方法PAR方法和程序證明器Dafny提出了一個(gè)模型驅(qū)動(dòng)的Dafny程序生成與驗(yàn)證方法,通過該方法對(duì)一些經(jīng)典問題進(jìn)行了算法形式化開發(fā)與自動(dòng)驗(yàn)證,大幅提高了所開發(fā)算法程序的可靠性。本文的主要工作包括:一、對(duì)Dafny自動(dòng)驗(yàn)證機(jī)理進(jìn)行了深入剖析并給出示例說明。二、探索出一種模型驅(qū)動(dòng)... 

【文章來源】：江西師范大學(xué)江西省

【文章頁數(shù)】：61 頁

【學(xué)位級(jí)別】：碩士

【部分圖文】：

軟件可信屬性圖

碩士學(xué)位論文4模型的的軟件開發(fā)三個(gè)發(fā)展階段。“模型驅(qū)動(dòng)”最早由OMG(對(duì)象管理組織)提出的MDA（model-drivenarchitecture）架構(gòu)而被人們熟知，MDA是一種基于UML和一系列標(biāo)準(zhǔn)的以模型為中心的開放框架，很好地支持不同應(yīng)用領(lǐng)域和技術(shù)平臺(tái)。模型驅(qū)動(dòng)的軟件開發(fā)是軟件工程一個(gè)重要研究方向，它開放性的理念和模式得到學(xué)術(shù)界和工業(yè)界的廣泛關(guān)注，而且它的優(yōu)點(diǎn)很多，包括有效提高軟件開發(fā)效率，增強(qiáng)軟件的可移植性，以及協(xié)同工作的能力和可維護(hù)性。下圖是各種開發(fā)技術(shù)的比較：圖1-2：軟件開發(fā)技術(shù)比較模型驅(qū)動(dòng)的軟件開發(fā)是當(dāng)前的研究熱點(diǎn)，已經(jīng)具備了相關(guān)技術(shù)基矗OMG推出了關(guān)于MOF(MetaObjectFacility,元對(duì)象機(jī)制)和MDA的規(guī)范，但MDA的可操作性研究還需進(jìn)一步發(fā)展。目前MDA開發(fā)工具市場(chǎng)現(xiàn)狀有：SDK開發(fā)商如Borland也推出了基于MDA的開發(fā)平臺(tái)，微軟也將MDA概念納入.NET開發(fā)平臺(tái)，但它們的開發(fā)期模型都是向自己的平臺(tái)映射。目前模型驅(qū)動(dòng)還有待研究的問題有：元模型和模型映射方法論研究、領(lǐng)域元模型的建立、模型映射技術(shù)的開發(fā)等[15]。1.2.2基于定理證明器的形式驗(yàn)證通過純手工形式結(jié)合一種形式驗(yàn)證方法(如Floyd斷言[16]、Hoare公理[17]等)對(duì)程序的正確性進(jìn)行驗(yàn)證的過程因?yàn)檫^于繁瑣復(fù)雜，很容易產(chǎn)生人為性錯(cuò)誤。形式驗(yàn)證通過定理證明和模型檢測(cè)兩種方法來提高用戶對(duì)規(guī)約和系統(tǒng)的可信度，定理證明以程序邏輯為基礎(chǔ)通過演繹推理的方式對(duì)命題開展證明。典型的基于定理證明的形式驗(yàn)證方法有Floyd-Hoare邏輯驗(yàn)證系統(tǒng)、Owicki和Gries的并發(fā)程序驗(yàn)證方法、Jones的Rely-Guarantee方法和并發(fā)分離邏輯[18]。因此對(duì)一些手工驗(yàn)證工作機(jī)械證明就有了定理證明器，它們?cè)谟布蛙浖?yàn)證上發(fā)揮了很大作用，通過將構(gòu)造證明過程轉(zhuǎn)換為編寫程序的過

碩士學(xué)位論文8圖2-1：最弱前置謂詞由圖可知，最弱的前提條件WP(c，B)任何狀態(tài)q都成立，q中的所有c后繼狀態(tài)均滿足B。用式子表示就是：qWP(c,B)iffq′∈Q.qC→q′q′B然后根據(jù)程序P的結(jié)構(gòu)遞歸的計(jì)算WP(P,B)。本文第三章在說明Dafny程序的內(nèi)在機(jī)理的時(shí)候?qū)⒊绦蜣D(zhuǎn)換為了GC程序，然后通過對(duì)GC程序應(yīng)用最弱前置謂詞規(guī)則一步步得到驗(yàn)證條件VC。具體的規(guī)則有以下這些：WP(assumeb,B)=bBWP(assertb,B)=b∧BWP(havocx,B)=B[a/x]WP(c1;c2,B)=WP(c1,WP(c2,B))WP(c1||c2,B)=WP(c1,B)∧WP(c2,B)2.2模型驅(qū)動(dòng)軟件開發(fā)方法隨著互聯(lián)網(wǎng)擴(kuò)展到社會(huì)的每個(gè)角落，由于平臺(tái)和技術(shù)工具的變革加快，出現(xiàn)了許多新的問題，如新平臺(tái)和應(yīng)用程序怎么與遺留系統(tǒng)互操作等，這些都是互聯(lián)網(wǎng)正面臨的新的挑戰(zhàn)。新技術(shù)不斷出現(xiàn)在新的應(yīng)用領(lǐng)域，組織如何確保其關(guān)鍵任務(wù)信息系統(tǒng)植根于適應(yīng)新硬件功能和軟件平臺(tái)的標(biāo)準(zhǔn)是研究的難點(diǎn)[26]。OMG（ObjectManagementGroup，即對(duì)象管理組織）通過模型驅(qū)動(dòng)架構(gòu)的MDA（ModelDrivenArchitecture）架構(gòu)解決了這一現(xiàn)實(shí)問題，MDA[20]是一種新的軟件系統(tǒng)開發(fā)的設(shè)計(jì)方法，核心是將系統(tǒng)應(yīng)用與其實(shí)現(xiàn)的技術(shù)平臺(tái)解耦。MDA方法的提出主要有三個(gè)目標(biāo)：一是改變以代碼為中心的軟件開發(fā)方法；二是解決不同平臺(tái)和技術(shù)路線之間的集成和互操作問題；三是適應(yīng)未來出現(xiàn)的新技術(shù)和新平臺(tái)。該架構(gòu)涉及的模型主要有計(jì)算無關(guān)的模型CIM（ComputationIndependentModel）、平臺(tái)無關(guān)模型PIM（PlatformIndependentModel）、平臺(tái)相關(guān)模型PSM（PlatformSpecificModel）和代碼[27]。從CIM、PIM、PSM到代碼，是一個(gè)從抽象到具體的過程。MDA的特點(diǎn)是將PIM到PSM的轉(zhuǎn)換自動(dòng)化了，然后PSM經(jīng)由MDA工具自動(dòng)生成代碼，極大提升了開發(fā)

【參考文獻(xiàn)】：
期刊論文
[1]軟件形式化驗(yàn)證專題前言[J]. 賀飛,張立軍.  軟件學(xué)報(bào). 2019(07)
[2]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明.  軟件學(xué)報(bào). 2019(01)
[3]算法的形式化推導(dǎo)與基于Isabelle的自動(dòng)化驗(yàn)證[J]. 齊蕾蕾,楊慶紅,游穎.  江西師范大學(xué)學(xué)報(bào)(自然科學(xué)版). 2018(04)
[4]WSDL→Radl-WS生成方法及自動(dòng)轉(zhuǎn)換系統(tǒng)[J]. 張琦,王昌晶,羅海梅,左正康,石海鶴,郭帆.  江西師范大學(xué)學(xué)報(bào)(自然科學(xué)版). 2018(03)
[5]“可信軟件基礎(chǔ)研究”重大研究計(jì)劃結(jié)題綜述[J]. 何積豐,單志廣,王戟,蒲戈光,房毓菲,劉克,趙瑞珍,張兆田.  中國科學(xué)基金. 2018(03)
[6]PAR平臺(tái)中若干軟件構(gòu)件形式化驗(yàn)證技術(shù)研究[J]. 胡啟敏,薛錦云,游珍,程著.  計(jì)算機(jī)工程與科學(xué). 2018(02)
[7]SMT求解技術(shù)的發(fā)展及最新應(yīng)用研究綜述[J]. 王翀,呂蔭潤(rùn),陳力,王秀利,王永吉.  計(jì)算機(jī)研究與發(fā)展. 2017(07)
[8]基于模型的自適應(yīng)方法綜述[J]. 趙天琪,趙海燕,張偉,金芝.  軟件學(xué)報(bào). 2018(01)
[9]基于分離邏輯的程序驗(yàn)證研究綜述[J]. 秦勝潮,許智武,明仲.  軟件學(xué)報(bào). 2017(08)
[10]基于KeY的程序分析和驗(yàn)證[J]. 夏新凱,陳冬火.  軟件. 2016(03)

碩士論文
[1]基于模型驅(qū)動(dòng)的WSDL→Radl-WS生成方法及自動(dòng)轉(zhuǎn)換系統(tǒng)[D]. 張琦.江西師范大學(xué) 2018
[2]遞推技術(shù)在算法設(shè)計(jì)中的應(yīng)用研究[D]. 張園.江西師范大學(xué) 2012
[3]基于PAR平臺(tái)的最弱前置謂詞生成器的設(shè)計(jì)與實(shí)現(xiàn)[D]. 楊晨.江西師范大學(xué) 2010
[4]PAR方法在組合數(shù)學(xué)問題中的應(yīng)用研究[D]. 孫凌宇.江西師范大學(xué) 2005



本文編號(hào)：2994583