基于項(xiàng)重寫(xiě)技術(shù)的規(guī)格和模型檢測(cè)研究.pdf

1、數(shù)學(xué)和邏輯中把一個(gè)公式中的某個(gè)子項(xiàng)替換成另一個(gè)子項(xiàng)的操作過(guò)程就是項(xiàng)重寫(xiě)。項(xiàng)重寫(xiě)系統(tǒng)的理論是計(jì)算的基礎(chǔ)理論。本文屬于項(xiàng)重寫(xiě)技術(shù)在形式化方法領(lǐng)域的應(yīng)用研究。主要貢獻(xiàn)在于:成功地把項(xiàng)重寫(xiě)的基本思想應(yīng)用在通用語(yǔ)言模型檢測(cè)當(dāng)中,給出基于通用語(yǔ)言源文件模型檢測(cè)的思想框架和具體方案,并最終用實(shí)驗(yàn)表明這個(gè)方案的可行性。這項(xiàng)工作建立在對(duì)項(xiàng)重寫(xiě)系統(tǒng)概念背景和發(fā)展歷史的考察基礎(chǔ)上,借鑒了現(xiàn)代主流形式化工具的設(shè)計(jì)思想,并充分利用現(xiàn)代通用編程語(yǔ)言的高級(jí)特性,使得

2、形式化建模更加容易。論文的全部工作包括:
　　項(xiàng)重寫(xiě)技術(shù)用于系統(tǒng)規(guī)格和模型檢測(cè)的實(shí)踐現(xiàn)代軟件技術(shù)的發(fā)展已經(jīng)把項(xiàng)重寫(xiě)系統(tǒng)的理論用于軟件實(shí)踐,一些功能比較完備的基于重寫(xiě)技術(shù)的程序設(shè)計(jì)語(yǔ)言和工具已經(jīng)被開(kāi)發(fā)出來(lái)。使用這樣的一種工具M(jìn)aude在系統(tǒng)規(guī)格和模型檢測(cè)方面做了一些實(shí)踐:嘗試用Maude表達(dá)Petri網(wǎng)模型,分析了軟件形式化中Maude代替Petri網(wǎng)的可能性;使用Maude的search命令和LTL工具進(jìn)行模型檢測(cè)實(shí)踐,并把模型檢

3、測(cè)方法用于求解智力游戲問(wèn)題;參考別人代碼基礎(chǔ)上,完成了對(duì)簡(jiǎn)單微處理器建立Maude模型的實(shí)踐。實(shí)踐表明,基于重寫(xiě)技術(shù)的軟件工具可以在一定程序上被當(dāng)做通用編程語(yǔ)言使用,而不是僅僅作為軟件形式化方法和軟件測(cè)試中的專門技術(shù)。
　　通用語(yǔ)言實(shí)現(xiàn)模型檢測(cè)命令式語(yǔ)言和基于重寫(xiě)技術(shù)的語(yǔ)言(函數(shù)式語(yǔ)言)在其發(fā)展過(guò)程中都在向?qū)Ψ綄W(xué)習(xí)借鑒,取長(zhǎng)補(bǔ)短。當(dāng)今流行的一些命令式編程語(yǔ)言(如 Python)也有函數(shù)式編程的語(yǔ)法風(fēng)格。嘗試使用通用語(yǔ)言直接對(duì)源文件