1、形式化方法是一種建立在嚴(yán)格數(shù)學(xué)基礎(chǔ)上的軟件開發(fā)方法。在軟件開發(fā)過程中使用形式化方法，既可以提高目標(biāo)軟件系統(tǒng)的正確性和可靠性，又能提高軟件的開發(fā)效率。但是，正因為形式方法以嚴(yán)格的數(shù)學(xué)理論為基礎(chǔ)，所以用它來描述的軟件需求規(guī)格說明比較抽象難懂。而且，一般來說，形式化的規(guī)格說明語言都是不可執(zhí)行的，用戶和領(lǐng)域?qū)＜覍π问交?guī)格說明及其符號方面的知識了解甚少，很難去理解形式化規(guī)格說明，也就難以確定規(guī)格說明是否與他們的需求相一致。為此，人們提出要對形式

2、化的需求規(guī)格說明進行確認(rèn)和驗證。 本文主要研究了軟件需求規(guī)格說明的一種確認(rèn)方法——動畫模擬技術(shù)，并最終研究開發(fā)了一個Object-Z規(guī)格說明動畫模擬系統(tǒng)——OZAnimator，該系統(tǒng)能夠模擬執(zhí)行Object-Z規(guī)格說明，幫助人們理解需求規(guī)格說明，從而實現(xiàn)對規(guī)格說明的一致性確認(rèn)。 首先，本文為Object-Z規(guī)格說明定義了一種通用的XML格式，動畫模擬系統(tǒng)將處理滿足該格式的Object-Z規(guī)格說明。 其次，在結(jié)構(gòu)

3、模擬部分，作者選擇SICStusProlog作為動畫模擬語言，根據(jù)Object-Z規(guī)格說明語言的語法語義，制定了一系列由Object-Z規(guī)格說明到Prolog文件的轉(zhuǎn)換規(guī)則，并使用XSLT描述出來。在動畫過程中，輸入的Object-Z規(guī)格說明將根據(jù)這些轉(zhuǎn)換規(guī)則自動轉(zhuǎn)換成可執(zhí)行的Prolog程序。 作者使用Java語言設(shè)計了一個良好的動畫模擬界面，該界面包含了Obiect-Z規(guī)格說明的文檔結(jié)構(gòu)、類的屬性和變化情況、用戶的操作過程以