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

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

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

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

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

5、模型檢驗(yàn)方法。此方法根據(jù)抽象解釋中抽象域的最小完備精化，來獲得CTL性質(zhì)強(qiáng)保留的最優(yōu)抽象模型，并且最優(yōu)抽象模型總是存在。首先通過狀態(tài)標(biāo)簽函數(shù)確定初始抽象域，然后通過不動點(diǎn)求解，得到對補(bǔ)集和標(biāo)準(zhǔn)前向轉(zhuǎn)換完備的最優(yōu)抽象域，也就是對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)空間爆炸問題。 ⑶為了自動演繹驗(yàn)證Statecharts，需對圖形化的Statecharts轉(zhuǎn)換為文本表示Statetxt，然后進(jìn)行驗(yàn)證。本文提出了一種在演繹驗(yàn)證不變式中輔助不變式的自動生成方法。描述了一個生成不變式和輔助謂詞的框架，從而驗(yàn)證時態(tài)安全性質(zhì)。為了保證搜索的收斂，通過對系統(tǒng)安全抽象來構(gòu)造近似系統(tǒng)。該方法為形式化驗(yàn)證Statecharts提供了一種新的思路。 ⑷為了

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