VDM-JML轉(zhuǎn)換方法的研究及其在軟件開發(fā)過程中的應(yīng)用.pdf

1、在軟件工程中,自然語言描述需求說明文檔的做法應(yīng)用廣泛,典型的如使用UML建模工具。但是,自然語言的多義性、上下文有關(guān)性、非系統(tǒng)性等特點(diǎn)致使其在描述復(fù)雜系統(tǒng)時(shí)可能引起語法二義性和系統(tǒng)的不一致性。為了保證軟件產(chǎn)品的可靠性,形式化方法應(yīng)運(yùn)而生。形式化方法采用形式規(guī)約語言精確地描述軟件規(guī)約說明,建立精確的、無二義性的語義,以數(shù)學(xué)的精確性保證了系統(tǒng)結(jié)構(gòu)的合理性、正確性和良好的可維護(hù)性。VDM是形式化的抽象模型方法中最具代表性的一種。它是一種功能構(gòu)

2、造性規(guī)格說明技術(shù),它的核心元素是其標(biāo)準(zhǔn)化規(guī)范語言VDM-SL。數(shù)學(xué)的精確性使它能夠有效地保證系統(tǒng)的設(shè)計(jì)和開發(fā),因而廣泛應(yīng)用于工業(yè)界的形式化系統(tǒng)開發(fā)。
　　JML是一種基于Java高級語言的形式的行為接口規(guī)范語言,它用來規(guī)范Java的模塊的行為和具體設(shè)計(jì)。JML的思想來自于Eiffel語言的契約式設(shè)計(jì)思想。目前基于JML的驗(yàn)證、調(diào)試和測試等支撐工具已經(jīng)比較成熟。本文分析了VDM-SL和JML這兩種抽象層次不同的規(guī)范語言,提出了從VD

3、M-SL語言到JML語言在常量、變量以及約束上的轉(zhuǎn)換策略。針對VDM-SL語言語法子集的BNF范式提出了VDM-SL規(guī)范到JML約束的轉(zhuǎn)換的設(shè)計(jì)方案,本文具體地分別描述了基本數(shù)據(jù)類型、集合操作、用戶自定義類型、狀態(tài)、類型約束、函數(shù)和運(yùn)算等有意義的VDM結(jié)構(gòu)到JML的映射機(jī)制。同時(shí),文章給出了基于上述VDM-JML映射機(jī)制的工具JML-SL to JML的實(shí)現(xiàn)框架。它是一個(gè)基于Eclipse平臺的插件,用來輔助用戶把VDM約束按照已定義好

4、的VDM-JML轉(zhuǎn)換機(jī)制映射到相應(yīng)的帶有JML規(guī)范注釋的Java程序。相應(yīng)的Java的模塊在后續(xù)的開發(fā)中由開發(fā)人員進(jìn)行實(shí)現(xiàn)。程序驗(yàn)證方面,本文利用了JML的測試工具間接地驗(yàn)證了VDM-SL的規(guī)范。VDM-JML的轉(zhuǎn)換的策略使得上層設(shè)計(jì)對下層開發(fā)的指導(dǎo)機(jī)制更加完善,因而構(gòu)造了一個(gè)貫穿于整個(gè)軟件生命周期的軟件開發(fā)方法。通過需求、架構(gòu)、設(shè)計(jì)、開發(fā)、測試等開發(fā)步驟的螺旋迭代,系統(tǒng)的軟件原型得以逐步求精,從而使得軟件的實(shí)現(xiàn)更加契合系統(tǒng)的設(shè)計(jì)思路。