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

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

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

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