基于SPIN的ATM交換機行為的驗證.pdf

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

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