傳統(tǒng)模型檢測技術(shù)主要采用時態(tài)邏輯描述被驗證的規(guī)范,人們較少注意多智能體認(rèn)知邏輯的模型檢測問題。而在分布式系統(tǒng)領(lǐng)域,系統(tǒng)和協(xié)議的規(guī)范很適合用認(rèn)知邏輯來描述。Web服務(wù)是一個典型的分布式系統(tǒng)。把Web服務(wù)組合建模為多智能體系統(tǒng),并成功采用我們實現(xiàn)的時態(tài)認(rèn)知邏輯符號模型檢測工具M(jìn)CTK驗證了SAS股票分析服務(wù)實例。同時采用WSAT,WS-Engineer和SPIN 3個模型檢測工具在相同實驗環(huán)境下驗證了該實例,實驗結(jié)果表明我們的Web服務(wù)模型檢測方法不僅比這3個模型檢測工具更高效,而且支持認(rèn)知邏輯規(guī)范的驗證,這是這3個模型檢測工具所不具備的。 

【文章來源】：計算機(jī)科學(xué). 2009,36(08)北大核心CSCD

【文章頁數(shù)】：5 頁

【部分圖文】：

SAS協(xié)議的通信模型

的方式進(jìn)行交互的情況。在這種共享方式下,共享變量被所有訪問它的智能體所觀察。SAS協(xié)議的智能體模塊處理流程如圖2所示。由于智能體模塊內(nèi)部的處理流程在MCTK中的描述機(jī)械冗長,篇幅所限,本文不羅列其中的具體細(xì)節(jié),重點關(guān)注每一智能體可觀察變量集合的定義。·155·

【參考文獻(xiàn)】：
期刊論文
[1]數(shù)據(jù)和時間感知的Web服務(wù)組合模型檢測[J]. 狄浩軍,戎玫,張廣泉,朱稷涵.  計算機(jī)科學(xué). 2011(11)



本文編號：3508421