形式化需求分析與自動(dòng)驗(yàn)證的研究與應(yīng)用.pdf

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

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