计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2011年
12期
139-143
,共5页
石慧娟%戎玫%张广泉%朱稷涵
石慧娟%戎玫%張廣泉%硃稷涵
석혜연%융매%장엄천%주직함
Web服务组合%XYZ/ADL%异步通信%时间属性%模型检测
Web服務組閤%XYZ/ADL%異步通信%時間屬性%模型檢測
Web복무조합%XYZ/ADL%이보통신%시간속성%모형검측
Web服务组合为研究对象,重点讨论了服务组合中异步通信行为和时间属性的形式化描述和验证.首先,从软件体系结构角度分析Web服务组合,采用基于时序逻辑的XYZ/ADL描述Web服务的交互行为和时间属性；然后,提出一种符合模型检测工具UPPAAL规约的时间异步通信模型TACM;最后,实现了XYZ/RE通信命令到TACM的映射,利用UPPAAL验证了服务组合系统异步通信行为的正确性.
Web服務組閤為研究對象,重點討論瞭服務組閤中異步通信行為和時間屬性的形式化描述和驗證.首先,從軟件體繫結構角度分析Web服務組閤,採用基于時序邏輯的XYZ/ADL描述Web服務的交互行為和時間屬性；然後,提齣一種符閤模型檢測工具UPPAAL規約的時間異步通信模型TACM;最後,實現瞭XYZ/RE通信命令到TACM的映射,利用UPPAAL驗證瞭服務組閤繫統異步通信行為的正確性.
Web복무조합위연구대상,중점토론료복무조합중이보통신행위화시간속성적형식화묘술화험증.수선,종연건체계결구각도분석Web복무조합,채용기우시서라집적XYZ/ADL묘술Web복무적교호행위화시간속성；연후,제출일충부합모형검측공구UPPAAL규약적시간이보통신모형TACM;최후,실현료XYZ/RE통신명령도TACM적영사,이용UPPAAL험증료복무조합계통이보통신행위적정학성.
