《網絡協議分析與設計》實驗報告書 實驗一

一、實驗目的 1.熟悉數據鏈路層協議，並能用PROMELA語言正確描述 2.掌握用SPIN驗證協議的方法 二、實驗原理 對於給定的一個使用PROMELA描述的協議系統，SPIN可以對其執行任意的模擬，也可以生成一個C代碼程序，然後對該系統的正確性進行有效檢驗，並報告系統中出現的死鎖，無效的循環，未定義的接受和標記不完全等情況。 三、實驗儀器 PC機 四、實驗內容 將 6.3 節描述的協議條件改爲：

>>阅读原文<<