基于SPIN的ATM交換機(jī)行為的驗(yàn)證.pdf

1、近些年來(lái)模型檢測(cè)已經(jīng)成為驗(yàn)證硬件設(shè)計(jì)正確性一種實(shí)用的方法，它能克服傳統(tǒng)方法(比如仿真和測(cè)試)的一些固有的缺陷，因?yàn)楦F盡的測(cè)試是不可能的并且也只能針對(duì)一些經(jīng)典的情況進(jìn)行測(cè)試。模型檢測(cè)用嚴(yán)格的數(shù)學(xué)方法來(lái)證明系統(tǒng)是否滿足給出的屬性。用模型檢測(cè)驗(yàn)證一個(gè)系統(tǒng)可分為兩個(gè)步驟： 1.用時(shí)態(tài)公式給出系統(tǒng)必須滿足的屬性 2.用模型檢測(cè)器給出系統(tǒng)的抽象模型并且驗(yàn)證時(shí)態(tài)屬性是否滿足 如果屬性不滿足，模型檢測(cè)器能給出反例，以便用戶能夠找

2、出系統(tǒng)發(fā)生邏輯錯(cuò)誤原因。 本文首先概要的介紹了形式化方法的分類(lèi)和發(fā)展歷史，然后又分析了模型檢測(cè)方法的基本概念和基本理論(其中包括CTL*,CTL，LTL,Kripe結(jié)構(gòu))。并且介紹了模型檢測(cè)器SPIN的基本結(jié)構(gòu)和基本使用以及SPIN接受的語(yǔ)言PROMELA的一些簡(jiǎn)單語(yǔ)法和語(yǔ)義。 最后在本文中我仔細(xì)分析了一個(gè)4*4端口的ATM交換機(jī)的抽象行為，用狀態(tài)圖描述了該交換機(jī)的行為。在給出這些行為的時(shí)候是高度抽象的，忽略了ATM的信