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

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

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

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

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

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

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

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