基于SPIN的命題投影時(shí)序邏輯模型檢查.pdf

1、目前軟件工業(yè)界面臨著產(chǎn)品功能越來(lái)越復(fù)雜和推出產(chǎn)品周期越來(lái)越短的雙重壓力。軟件工程的一個(gè)主要目標(biāo)就是在復(fù)雜性增加的情況下仍能構(gòu)造正確可靠的系統(tǒng)。為了達(dá)到上述目標(biāo)，形式化方法在軟件開(kāi)發(fā)中得到了廣泛的應(yīng)用，特別是模型檢查技術(shù)。 本文提出了一種基于SPIN的命題投影時(shí)序邏輯的模型檢查方法。 在此方法中，系統(tǒng)的性質(zhì)用命題投影時(shí)序邏輯公式來(lái)描述，隨后這個(gè)公式被轉(zhuǎn)換為其永非斷言； 然后系統(tǒng)模型用Buchi自動(dòng)機(jī)來(lái)刻畫(huà)；

2、 最后通過(guò)SPIN完成模型檢查，即檢查系統(tǒng)是否滿(mǎn)足期望的性質(zhì)。 為了實(shí)現(xiàn)這一目的，文中設(shè)計(jì)并實(shí)現(xiàn)了命題投影時(shí)序邏輯公式的解釋轉(zhuǎn)換器，以便將命題投影時(shí)序邏輯公式自動(dòng)轉(zhuǎn)換為Promela形式的永非斷言。該轉(zhuǎn)換器首先將待驗(yàn)證的命題投影時(shí)序邏輯公式轉(zhuǎn)換為其正則式以及正則圖，然后通過(guò)正則圖可以得到所需的永非斷言。將該轉(zhuǎn)換器與模型檢查器SPIN相結(jié)合，使用命題投影時(shí)序邏輯公式來(lái)在SPIN中描述系統(tǒng)的性質(zhì)，這樣基于命題投影時(shí)序邏輯的模型檢查就