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

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

2、造性規(guī)格說明技術,它的核心元素是其標準化規(guī)范語言VDM-SL。數(shù)學的精確性使它能夠有效地保證系統(tǒng)的設計和開發(fā),因而廣泛應用于工業(yè)界的形式化系統(tǒng)開發(fā)。
　　JML是一種基于Java高級語言的形式的行為接口規(guī)范語言,它用來規(guī)范Java的模塊的行為和具體設計。JML的思想來自于Eiffel語言的契約式設計思想。目前基于JML的驗證、調(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ù)類型、集合操作、用戶自定義類型、狀態(tài)、類型約束、函數(shù)和運算等有意義的VDM結(jié)構到JML的映射機制。同時,文章給出了基于上述VDM-JML映射機制的工具JML-SL to JML的實現(xiàn)框架。它是一個基于Eclipse平臺的插件,用來輔助用戶把VDM約束按照已定義好

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