基于Promela的組合抽象Spin模型檢測(cè)及應(yīng)用.pdf

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

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

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