Statecharts及其時(shí)間擴(kuò)展的形式化驗(yàn)證技術(shù)研究.pdf

1、模型檢驗(yàn)是一種非常重要的自動(dòng)驗(yàn)證方法，主要通過(guò)顯式狀態(tài)搜索或隱式不動(dòng)點(diǎn)計(jì)算來(lái)驗(yàn)證有窮狀態(tài)系統(tǒng)的模態(tài)命題性質(zhì)，避免建立復(fù)雜的證明過(guò)程，并在不滿足性質(zhì)時(shí)能提供反例。二十多年來(lái)，人們對(duì)它進(jìn)行了廣泛而深入的研究，取得了許多研究成果，使得它在軟硬件驗(yàn)證等方面得到廣泛應(yīng)用，受到了廣大研究和開(kāi)發(fā)人員的高度重視。 本文主要針對(duì)Statecharts及其時(shí)間擴(kuò)展的形式化驗(yàn)證進(jìn)行研究，研究工作包括：(1)通過(guò)對(duì)Statecharts和模型檢驗(yàn)理論的

2、研究，給出了平坦化和非平坦化的模型檢驗(yàn)算法；(2)基于抽象解釋框架的性質(zhì)強(qiáng)保留的抽象模型檢測(cè)；(3)把圖形化的 Statecharts轉(zhuǎn)換為義本表示的Statetxt，從而演繹驗(yàn)證Statecharts；(4)對(duì)連續(xù)時(shí)間擴(kuò)展的Statecharts模型檢驗(yàn)進(jìn)行了研究和探索。主要成果表現(xiàn)在以下幾個(gè)方面： ⑴通常模型檢驗(yàn)Statecharts是先對(duì)其平坦化，然后使用已有模型檢驗(yàn)工具進(jìn)行驗(yàn)證。本文對(duì)傳統(tǒng)的 Statecharts模型檢

3、驗(yàn)方法進(jìn)行了改進(jìn)，提出了一種針對(duì)Statecharts語(yǔ)義的平坦化模型檢驗(yàn)方法。該方法基于Statecharts的操作語(yǔ)義和statecharts到LTS轉(zhuǎn)換規(guī)則，得到標(biāo)簽轉(zhuǎn)換系統(tǒng)LTS；在此基礎(chǔ)上，對(duì)LTS進(jìn)行符號(hào)表示，然后基于導(dǎo)向集的前向狀態(tài)搜索算法，符號(hào)檢驗(yàn)Statecharts模型是否滿足CTL公式的性質(zhì)。通過(guò)狀態(tài)搜索的導(dǎo)向集和狀態(tài)空間的符號(hào)表示，比較有效的縮減了需驗(yàn)證的狀態(tài)窄間。為了進(jìn)一步解決狀態(tài)空間爆炸問(wèn)題，又提出了一種非平

4、坦化的模型檢驗(yàn)方法，基于自動(dòng)機(jī)理論及Statecharts的操作語(yǔ)義，避免構(gòu)造平坦化過(guò)程，縮減狀念窄間體積，并通過(guò)可達(dá)性分析和環(huán)路檢測(cè)，直接對(duì)分層的Statecharts進(jìn)行模型檢驗(yàn)，驗(yàn)證其線性時(shí)態(tài)邏輯性質(zhì)。非平坦化的方法能避免因Statecharts平坦化而引起的狀態(tài)空間爆炸問(wèn)題。 ⑵為了進(jìn)一步研究Statecharts平坦化的模型檢驗(yàn)方法，基于抽象解釋的理論，以及完備抽象解釋和性質(zhì)強(qiáng)保留之間的關(guān)系，提出了一種性質(zhì)強(qiáng)保留的抽象

5、模型檢驗(yàn)方法。此方法根據(jù)抽象解釋中抽象域的最小完備精化，來(lái)獲得CTL性質(zhì)強(qiáng)保留的最優(yōu)抽象模型，并且最優(yōu)抽象模型總是存在。首先通過(guò)狀態(tài)標(biāo)簽函數(shù)確定初始抽象域，然后通過(guò)不動(dòng)點(diǎn)求解，得到對(duì)補(bǔ)集和標(biāo)準(zhǔn)前向轉(zhuǎn)換完備的最優(yōu)抽象域，也就是對(duì)CTL標(biāo)準(zhǔn)算子完備的最小抽象域，依據(jù)此抽象域求解CTL性質(zhì)強(qiáng)保留的最優(yōu)抽象狀態(tài)劃分。在抽象狀態(tài)劃分之間定義抽象轉(zhuǎn)換關(guān)系，構(gòu)造CTL性質(zhì)強(qiáng)保留的抽象模型。并指出了抽象域?qū)TL標(biāo)準(zhǔn)算子是完備的當(dāng)且儀當(dāng)抽象域?qū)ρa(bǔ)集和標(biāo)

6、準(zhǔn)前向轉(zhuǎn)換是完備的。此方法比較有效的解決了狀態(tài)空間爆炸問(wèn)題。 ⑶為了自動(dòng)演繹驗(yàn)證Statecharts，需對(duì)圖形化的Statecharts轉(zhuǎn)換為文本表示Statetxt，然后進(jìn)行驗(yàn)證。本文提出了一種在演繹驗(yàn)證不變式中輔助不變式的自動(dòng)生成方法。描述了一個(gè)生成不變式和輔助謂詞的框架，從而驗(yàn)證時(shí)態(tài)安全性質(zhì)。為了保證搜索的收斂，通過(guò)對(duì)系統(tǒng)安全抽象來(lái)構(gòu)造近似系統(tǒng)。該方法為形式化驗(yàn)證Statecharts提供了一種新的思路。 ⑷為了

7、使Statecharts能描述連續(xù)時(shí)間的能力，本文精確定義了連續(xù)時(shí)間擴(kuò)展的時(shí)間Statecharts，并提出了一種模型檢驗(yàn)時(shí)間Statecharts的方法。采用項(xiàng)代數(shù)表示時(shí)間Statecharts和進(jìn)程代數(shù)描述其并發(fā)行為，根據(jù)其一步語(yǔ)義及轉(zhuǎn)換規(guī)則，把時(shí)間Statecharts映射為時(shí)間自動(dòng)機(jī)，從而對(duì)時(shí)間Statecharts模型檢的問(wèn)題轉(zhuǎn)換為對(duì)時(shí)間自動(dòng)機(jī)的模型檢驗(yàn)。為了克服了連續(xù)時(shí)間的無(wú)窮問(wèn)題，通過(guò)抽象技術(shù)來(lái)獲得有限狀態(tài)空間，并給出了抽