針對(duì)SOFL形式化軟件規(guī)格說(shuō)明書(shū)完備性的自動(dòng)檢測(cè)方法研究.pdf

1、隨著 SOFL形式化軟件開(kāi)發(fā)方法的不斷發(fā)展，由于其更能夠?qū)崿F(xiàn)完整的、系統(tǒng)的形式化軟件規(guī)格說(shuō)明書(shū)，且不同于太復(fù)雜而難以實(shí)用的Z和VDM等形式化語(yǔ)言，SOFL能夠更加簡(jiǎn)單地被一般軟件開(kāi)發(fā)者使用從而發(fā)揮其高嚴(yán)密性的特長(zhǎng)以促進(jìn)傳統(tǒng)軟件開(kāi)發(fā)技術(shù)的有效性和系統(tǒng)性，因而被認(rèn)為是一種有效的軟件形式化開(kāi)發(fā)方法。在 SOFL方法中，撰寫(xiě)形式化規(guī)格書(shū)被當(dāng)作是幫助開(kāi)發(fā)者來(lái)充分理解軟件需求并為后期的軟件代碼實(shí)現(xiàn)提供堅(jiān)實(shí)基礎(chǔ)的一個(gè)方法。然而，檢測(cè)完備性至今依舊是一

2、個(gè)待解決的開(kāi)放性問(wèn)題。為了確保規(guī)格書(shū)涵蓋了所有的用戶(hù)需求，完備性，作為規(guī)格書(shū)的重要屬性之一，需要被檢測(cè)。本文就提出了一個(gè)基于工具的SOFL形式化軟件規(guī)格書(shū)的自動(dòng)檢測(cè)方法。
　　在文中，我們首先介紹用 SOFL語(yǔ)言撰寫(xiě)的形式化規(guī)格書(shū)的相關(guān)概念，然后解釋如何來(lái)實(shí)現(xiàn)形式化規(guī)格書(shū)完備性的自動(dòng)檢測(cè)。檢測(cè)完備性，即要檢測(cè)所有功能路徑覆蓋了全部需求，與此同時(shí)，任意兩條功能路徑必須是互斥的、沒(méi)有覆蓋的，也就是說(shuō)，要同時(shí)證明完整性和互斥性才能保證完