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

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