基于雙格的多值模型精化關(guān)系及對(duì)稱化簡(jiǎn).pdf

1、模型檢測(cè)是一種自動(dòng)驗(yàn)證系統(tǒng)行為屬性的技術(shù)。傳統(tǒng)的模型檢測(cè)針對(duì)基于布爾邏輯建立的系統(tǒng)模型,要求對(duì)系統(tǒng)的所有行為給予確定的描述。然而,在軟件開(kāi)發(fā)的許多階段,如在需求分析階段,由于用戶的要求不明確以及觀點(diǎn)的不一致,模型中可能包含不確定或不一致信息,傳統(tǒng)布爾模型無(wú)法滿足此要求,而多值模型更適合在此類情況下進(jìn)行建模和分析。多值模型一般采用基于德摩根代數(shù)的多值邏輯來(lái)定義,是傳統(tǒng)布爾模型的擴(kuò)展。與傳統(tǒng)模型檢測(cè)類似,多值模型檢測(cè)也存在狀態(tài)爆炸問(wèn)題。精化

2、關(guān)系是采用抽象和對(duì)稱化簡(jiǎn)等方法解決狀態(tài)爆炸問(wèn)題的基礎(chǔ),用來(lái)刻畫系統(tǒng)的具體模型和約簡(jiǎn)模型之間相對(duì)于時(shí)序邏輯所描述的行為屬性的保持關(guān)系。現(xiàn)有的針對(duì)多值模型的精化關(guān)系定義過(guò)強(qiáng),適用范圍受到限制。因此,我們提出了一種新的更加通用的多值模型精化關(guān)系,并且以此為基礎(chǔ)研究了多值模型的對(duì)稱化簡(jiǎn)方法。
　　我們以世界雙格作為理論基礎(chǔ),其中的邏輯值之間存在兩種序關(guān)系:真值序關(guān)系與信息序關(guān)系。任意一個(gè)德摩根代數(shù)均同構(gòu)于世界雙格的一個(gè)子格;同時(shí),對(duì)行為屬

3、性的模型檢測(cè)可根據(jù)邏輯值的真值序關(guān)系定義,而模型檢測(cè)結(jié)果的精確度以及具體模型和約簡(jiǎn)模型之間的屬性保持關(guān)系則可根據(jù)邏輯值的信息序關(guān)系定義。為此,我們首先定義了基于世界雙格的多值模型,以及時(shí)序邏輯μ演算所對(duì)應(yīng)的語(yǔ)義。然后,我們從兩個(gè)角度刻畫了新的多值模型的精化關(guān)系:(i)通過(guò)將多值模型分解為三值模型進(jìn)行刻畫,(ii)直接針對(duì)多值模型的結(jié)構(gòu)進(jìn)行刻畫;證明了這兩種刻畫等價(jià),是具體模型與約簡(jiǎn)模型滿足對(duì)μ演算公式的模型檢測(cè)保持信息序關(guān)系的充分必要條