模型檢測[自動驗證技術]

基本信息

• 中文名：模型檢測
• 英文名：model checking

模型檢測(model checking)是一種很重要的自動驗證技術。它最早由Clarke和Emerson以及Quielle和Sifakis在1981年分別提出，主要通過顯式狀態搜尋或隱式不動點計算來驗證有窮狀態並發系統的模態/命題性質。由於模型檢測可以自動執行，並能在系統不滿足性質時提供反例路徑，因此在工業界比演繹證明更受推崇。儘管限制在有窮系統上是一個缺點，但模型檢測可以套用於許多非常重要的系統，如硬體控制器和通信協定等有窮狀態系統。很多情況下，可以把模型檢測和各種抽象與歸納原則結合起來驗證非有窮狀態系統(如實時系統)。

模型檢測的基本思想是用狀態遷移系統(S)表示系統的行為，用模態邏輯公式(F)描述系統的性質。這樣“系統是否具有所期望的性質”就轉化為數學問題“狀態遷移系統S是否是公式F的一個模型”，用公式表示為S╞F。對有窮狀態系統，這個問題是可判定的，即可以用電腦程式在有限時間內自動確定。

模型檢測已被套用於計算機硬體、通信協定、控制系統、安全認證協定等方面的分析與驗證中，取得了令人矚目的成功，並從學術界輻射到了產業界。