從UML建模到Z形式化規(guī)范的研究.pdf

1、近幾年，計(jì)算機(jī)軟件發(fā)展迅速，越來越多的人們希望把問題交給計(jì)算機(jī)來解決，但其現(xiàn)狀還不能令人滿意。主要是軟件系統(tǒng)的規(guī)模以及復(fù)雜程度越來越高，但隨之帶來的軟件系統(tǒng)的出錯(cuò)率卻在不斷增加，整體功能差，效率低下。越來越多的災(zāi)難背后所隱藏的軟件問題也逐漸進(jìn)入人們的視線。所以軟件工程領(lǐng)域開始高度關(guān)注如何在軟件復(fù)雜性不斷增加的情況下，既能夠提高軟件的可靠性，同時(shí)又不降低軟件質(zhì)量。
　　 統(tǒng)一建模語(yǔ)言(UML)是一種標(biāo)準(zhǔn)的面向?qū)ο蟮膱D形化的建模語(yǔ)言

2、。UML支持面向?qū)ο蟮姆治雠c設(shè)計(jì)，其簡(jiǎn)單易懂的表述各種元模型，提供了大量基本的表示模型元素的圖形方法，能夠?qū)浖M(jìn)行可視化處理、描述和構(gòu)造等。UML模型作為一種圖形化語(yǔ)言，具有一定的優(yōu)點(diǎn)，能夠清晰地表示系統(tǒng)的邏輯模型或?qū)崿F(xiàn)模型。正是因?yàn)檫@些優(yōu)點(diǎn)，人們?cè)陂_發(fā)各種復(fù)雜的軟件系統(tǒng)的時(shí)候都是使用UML對(duì)系統(tǒng)進(jìn)行建模。
　　 形式化方法(Formal Method)能夠產(chǎn)生嚴(yán)密、準(zhǔn)確的軟件需求規(guī)格說明，一般情況下形式化方法都是存在于嚴(yán)格的

3、數(shù)學(xué)基礎(chǔ)和證明之上。在軟件設(shè)計(jì)領(lǐng)域人們對(duì)于軟件系統(tǒng)進(jìn)行規(guī)范、設(shè)計(jì)和編碼普遍的方法就是Z語(yǔ)言形式化規(guī)范。隨著Z形式化規(guī)范的發(fā)展和成熟，已經(jīng)被成功地應(yīng)用到許多關(guān)鍵性的工業(yè)軟件開發(fā)項(xiàng)目中。因此本文使用Z形式化方法對(duì)UML類圖到形式化方法的轉(zhuǎn)換。其最大的優(yōu)點(diǎn)在于可以形成無二義性的、精確的形式規(guī)約，并可以進(jìn)行模型驗(yàn)證或定理證明。形式化方法的這一特點(diǎn)不僅可以提高軟件開發(fā)的生產(chǎn)效率，同時(shí)可以大大提高軟件的可靠性。
　　 本文結(jié)合統(tǒng)一建模語(yǔ)言U