基于Promela的組合抽象Spin模型檢測及應用.pdf

1、模型檢測是一種重要的形式化驗證技術(shù)，能自動地檢驗系統(tǒng)是否滿足所期望的性質(zhì)。模型檢測已經(jīng)被成功地應用于計算機硬件、通信協(xié)議、控制系統(tǒng)和安全認證等方面的分析與驗證中。 模型檢測面臨的主要問題是狀態(tài)空間爆炸問題，因為其是對狀態(tài)空間的窮舉搜索，對于并發(fā)系統(tǒng)，狀態(tài)數(shù)隨著并發(fā)分量的增加而呈指數(shù)級的增長。組合和抽象方法可以將系統(tǒng)抽象成一個有窮狀態(tài)模型，去掉不影響待驗證性質(zhì)的細節(jié)，用盡可能少的狀態(tài)描述系統(tǒng)運行過程。從而降低模型檢測復雜性，在一定

2、程度上緩解狀態(tài)空間爆炸問題。 本文提出了組合抽象框架，對框架做出理論分析，指出了框架的適應范圍。通過建立各個主體的Kripke結(jié)構(gòu)，擴展了組合抽象方法，基于LTL性質(zhì)將其轉(zhuǎn)化為抽象的Kripke結(jié)構(gòu)，再組合抽象模型，最后運用模型檢測工具Spin進行檢測，以達到減少驗證時產(chǎn)生的狀態(tài)數(shù)的目的。詳細分析了Promela模型的本身特點，通過對協(xié)議的Promela模型Spin模型檢測，提出降低模型檢測的復雜性方法。結(jié)果表明，組合抽象框架可

3、以緩解狀態(tài)空間爆炸問題，運用atomic和降低proctype進程的個數(shù)的方法，可以降低模型檢測的復雜性。 在以上工作的基礎上，本文以NSPK協(xié)議為實例，建立了NSPK協(xié)議的Promela模型，運用Spin檢測LTL性質(zhì)，并對檢測結(jié)果進行分析，指出了NSPK協(xié)議的缺陷，并且對修改后的NSPK也進行檢測分析。對于多主體參與的協(xié)議，首先建立Kripke結(jié)構(gòu)，再抽象組合，最后對比組合抽象前后狀態(tài)數(shù)的變化，說明了組合抽象框架的可行性。對