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

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

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