基于交際接口的Web應(yīng)用模型檢驗

Web應(yīng)用作為最典型的網(wǎng)絡(luò)應(yīng)用已經(jīng)廣泛應(yīng)用于各個方面，如網(wǎng)上銀行、電子商務(wù)、時事新聞、工業(yè)生產(chǎn)、智能建筑等。Web應(yīng)用是否可靠逐漸引起人們關(guān)注。形式化驗證方法是提高軟件質(zhì)量的重要途徑。模型檢驗是一種可自動執(zhí)行的形式化分析和驗證技術(shù)。通過隱式不動點計算或顯式狀態(tài)搜索來驗證系統(tǒng)的性質(zhì)，并能在系統(tǒng)不滿足性質(zhì)時提供反例，已經(jīng)在硬件和軟件驗證等領(lǐng)域取得很大成功。