形式化需求分析與自動驗證的研究與應用.pdf

1、隨著計算機技術的發(fā)展以及企業(yè)的進步，軟件開發(fā)者不斷運用新技術和新思想對傳統(tǒng)的管理軟件進行改進，如何開發(fā)一款操作方便且功能完善的軟件以滿足客戶的要求，成為現(xiàn)代軟件開發(fā)人員必須面對的問題。UML是一種傳統(tǒng)的非形式化需求分析的方法，已經(jīng)廣泛應用于軟件開發(fā)的各個階段，但是其擁有非形式化的共同缺陷：需求獲取交流困難、分析建模周期過長以及容易產(chǎn)生歧義性。形式化需求分析和軟件規(guī)范說明技術就是在需求獲取的基礎上用建立系統(tǒng)的邏輯模型，從而對復雜問題進行分

2、析和抽象，最終將用戶需求轉(zhuǎn)化成軟件規(guī)范說明的方法。然而，形式化描述需要很強的專業(yè)知識，這樣嚴重阻礙其廣泛應用。
　　 本文采用B方法形式規(guī)約語言對UML模型圖進行形式化描述，并給出了一組和UML對應的數(shù)學模型方法，實現(xiàn)UML模型圖到B方法形式規(guī)約的轉(zhuǎn)換。文中，主要對類圖和狀態(tài)圖的組成元素進行分析，將它們轉(zhuǎn)換為對應的B方法模型，通過B方法支持工具對所得到的形式規(guī)約進行一致性檢測、動態(tài)分析和模型檢測，并結合人事信息管理系統(tǒng)實例說明了