基于SPIN的SOCKET通信程序分析系統(tǒng).pdf

1、形式化方法是驗證并發(fā)系統(tǒng)可靠性和安全性的一種手段。模型檢測是一種對有限狀態(tài)并發(fā)(分布式)系統(tǒng)進行形式化驗證的方法,已應用于軟件可靠性和安全性驗證。從用高級語言開發(fā)的并發(fā)軟件系統(tǒng)中自動抽取模型,使用模型檢測工具對所抽取的模型進行驗證是模型檢測技術領域中的一個研究熱點。基于TCP/IP協(xié)議的socket(套接字)通信程序可靠性是互聯(lián)網(wǎng)數(shù)據(jù)傳輸?shù)闹匾A。本文圍繞socket通信程序(C語言開發(fā))可靠性問題,研究基于模型檢測工具SPIN的so

2、cket通信程序分析與驗證技術,主要工作及成果有:
　　 1.分析socket通信程序中socket函數(shù)調用順序正確性,即對已通過語法檢查及編譯,但由于服務和客戶程序中socket函數(shù)調用順序異常而導致的程序運行時潛在問題(死鎖、內存泄漏、邊界數(shù)據(jù)丟失及其它運行時錯誤)進行檢測。
　　 2.針對socket函數(shù)調用順序正確性問題,設計從socket程序源代碼抽取模型方案。通過分析socket程序的順序結構,提出socke

3、t通信程序中socket函數(shù)調用序列抽取算法;定義Prometa消息數(shù)據(jù)結構和通道;規(guī)約socket函數(shù)的Promela模型;定義socket函數(shù)到Promela映射規(guī)則;提出目標Promela模型生成算法,并對模型應滿足的性質用線性時態(tài)邏輯(LTL)進行規(guī)約。
　　 3.采用原子序列atomic、偏序規(guī)約、Bit-statehashing等策略以提高驗證效率,有效地壓縮驗證過程中的狀態(tài)空間和存儲空間。
　　 4.設計并