UML用例模型的B形式化描述方法研究.pdf

1、隨著信息技術的飛速發(fā)展，計算機軟件系統(tǒng)的應用逐漸擴展到了社會的各個領域。軟件規(guī)模和復雜度在不斷增加，軟件出現錯誤的可能性也隨之增加。如何保證軟件的質量、提高軟件的可靠性，已成為目前軟件工程研究領域的一個熱點。將形式化方法和主流的軟件開發(fā)方法相結合是一種可行的方法。 UML作為當前比較流行的一種可視化建模語言，已成為面向對象分析和設計中事實上的工業(yè)標準。UML模型直觀、易懂，利于開發(fā)者與用戶之間的溝通。但UML的大部分語義是用自然

2、語言描述的，確乏精確的語義，容易產生模糊或歧義；UML缺乏有效的推理機制和完善的模型檢查能力，不便于使用工具對其描述的規(guī)約進行動態(tài)分析和驗證。形式化方法則是基于嚴格數學理論的，能產生精確、無二義性的形式規(guī)約，為軟件開發(fā)提供了嚴格的數學基礎，這對提高軟件的可靠性有著非常顯著的作用。但形式規(guī)約不夠直觀，可讀性較差，不便于與用戶進行交流，要求開發(fā)者具有良好的數學基礎。因此，形式化方法的研究和應用目前仍局限在較小的范圍之內。把形式化方法和UML

3、相結合實現優(yōu)勢互補的研究對保證軟件質量、提高可靠性有著非常重要的意義。 本文選擇B方法作為形式規(guī)約方法，把UML模型的圖形規(guī)約映射到B形式規(guī)約。一方面，我們能夠借助于強大的B方法支持工具，基于相應的B形式規(guī)約，對UML建模結果進行正確性分析和一致性檢查；另一方面，可將UML規(guī)約作為形式化開發(fā)的基礎，降低直接使用B方法建立形式規(guī)約的難度，增強B方法在軟件開發(fā)中的實際作用。 本文以UML用例模型為主要研究對象，在分析UML用

4、例模型概念和B抽象機符號的基礎上，對用例模型建模元素的抽象語法進行描述，建立兩者之間的映射，實現UML用例模型圖到B形式規(guī)約的轉換。軟件開發(fā)人員可以首先用半形式化的UML用例模型為目標系統(tǒng)建立需求模型，然后根據文中給出方法構建目標系統(tǒng)的B形式化規(guī)約，再利用B方法支持工具對規(guī)約進行動態(tài)分析和模型驗證，得出可靠的形式規(guī)約，為在此基礎上進行的形式推導和精化提供了正確的起點。最后，通過對電梯控制系統(tǒng)的實例分析，進一步詳述了UML用例模型到B方法