计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2012年
6期
129-132
,共4页
限界模型检查%Web服务%行为失配检测%可满足性模理论
限界模型檢查%Web服務%行為失配檢測%可滿足性模理論
한계모형검사%Web복무%행위실배검측%가만족성모이론
在Web服务组合过程中,常因交互协议不一致等导致服务失配；Web服务失配检测可准确捕捉失配点,为实现服务的有效组合奠定基础.采用限界模型检查技术,提出一种基于可满足性模理论(SMT)的Web服务行为失配检测方法.该方法首先将服务失配检测问题转化为逻辑公式的可满足性判定问题,然后利用Yices工具实现Web服务行为失配检测,最后通过实例进一步阐述该方法的有效性.
在Web服務組閤過程中,常因交互協議不一緻等導緻服務失配；Web服務失配檢測可準確捕捉失配點,為實現服務的有效組閤奠定基礎.採用限界模型檢查技術,提齣一種基于可滿足性模理論(SMT)的Web服務行為失配檢測方法.該方法首先將服務失配檢測問題轉化為邏輯公式的可滿足性判定問題,然後利用Yices工具實現Web服務行為失配檢測,最後通過實例進一步闡述該方法的有效性.
재Web복무조합과정중,상인교호협의불일치등도치복무실배；Web복무실배검측가준학포착실배점,위실현복무적유효조합전정기출.채용한계모형검사기술,제출일충기우가만족성모이론(SMT)적Web복무행위실배검측방법.해방법수선장복무실배검측문제전화위라집공식적가만족성판정문제,연후이용Yices공구실현Web복무행위실배검측,최후통과실례진일보천술해방법적유효성.
