UML狀態(tài)圖的形式化研究.pdf

1、從上世紀(jì)五十年代軟件誕生開(kāi)始，軟件設(shè)計(jì)一直是軟件系統(tǒng)開(kāi)發(fā)的核心內(nèi)容，好的軟件設(shè)計(jì)有助于軟件開(kāi)發(fā)人員提高工作效率，減少不必要的開(kāi)支以及保證軟件的正確性。但采用何種方法來(lái)保證軟件設(shè)計(jì)是“好的”
　　 一直是軟件開(kāi)發(fā)人員關(guān)注的問(wèn)題。從最初靠個(gè)人智慧來(lái)設(shè)計(jì)和編寫軟件，到各種軟件設(shè)計(jì)方法“百家爭(zhēng)鳴”，再到眾所周知的統(tǒng)一建模語(yǔ)言，研究者們一直試圖找到一種理想的設(shè)計(jì)方法一這種設(shè)計(jì)方法易于被使用者理解和接受，便于使用和交流，規(guī)范且能保證設(shè)計(jì)的正

2、確性，這種語(yǔ)言至今并未出現(xiàn)，目前的設(shè)計(jì)語(yǔ)言只能滿足上述部分方面。到了上世紀(jì)末，出現(xiàn)了兩種風(fēng)格迥異的設(shè)計(jì)方法，一種方法提倡簡(jiǎn)單靈活，既不使用復(fù)雜的數(shù)學(xué)理論作為基礎(chǔ)，也不使用嚴(yán)謹(jǐn)?shù)脑O(shè)計(jì)方式保證正確性，這種方法就是已經(jīng)被大多數(shù)設(shè)計(jì)人員和團(tuán)隊(duì)接受的統(tǒng)一建模語(yǔ)言；另一種方法認(rèn)為在軟件設(shè)計(jì)階段用精確和嚴(yán)謹(jǐn)?shù)淖C明保證系統(tǒng)的正確性是必不可少的，提倡采用規(guī)范可證明方式來(lái)設(shè)計(jì)軟件。但由于需要使用者具有較好的數(shù)學(xué)基礎(chǔ)，普及成本較高，加上技術(shù)并不成熟以及沒(méi)有好

3、的工具支持，使得這種方法目前仍處于試驗(yàn)階段，并未普及，如VDM方法、B方法、Z方法等。
　　 本文提出了一種使用CHAM化學(xué)抽象機(jī)形式化語(yǔ)言對(duì)狀態(tài)圖進(jìn)行形式化的方法，之所以選擇化學(xué)抽象機(jī)形式化語(yǔ)言，因?yàn)檫@種語(yǔ)言最初用于并行計(jì)算的描述，具有嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)基礎(chǔ)和完整的語(yǔ)義，之后，用于系統(tǒng)行為的描述，具有一定的動(dòng)態(tài)描述能力，有可能實(shí)現(xiàn)狀態(tài)圖的形式化，本文采用一種新的狀態(tài)圖的劃分方法，將狀態(tài)圖分為簡(jiǎn)單狀態(tài)圖，分層狀態(tài)圖和并發(fā)狀態(tài)圖三種，并分