计算机科学
計算機科學
계산궤과학
COMPUTER SCIENCE
2010年
11期
122-125
,共4页
Web服务组合%模型检测%XYZ/ADL%XYZ/RE%UPPAAL
Web服務組閤%模型檢測%XYZ/ADL%XYZ/RE%UPPAAL
Web복무조합%모형검측%XYZ/ADL%XYZ/RE%UPPAAL
Web服务组合的正确性验证对提高软件开发效率、实现服务增值具有重要意义.为从高层抽象层次研究Web服务组合的正确性及其形式化验证方法,考虑到Web服务组合中的实时特征,在采用软件体系结构描述语言XYZ/ADL对Web服务组合进行描述的基础上,将其实时描述部分XYZ/RE转换至时间自动机模型,组合后系统应满足的性质用分支时序逻辑CTL公式表示,最后应用模型检测工具UPPAAL实现了Web服务组合正确性的自动化验证.
Web服務組閤的正確性驗證對提高軟件開髮效率、實現服務增值具有重要意義.為從高層抽象層次研究Web服務組閤的正確性及其形式化驗證方法,攷慮到Web服務組閤中的實時特徵,在採用軟件體繫結構描述語言XYZ/ADL對Web服務組閤進行描述的基礎上,將其實時描述部分XYZ/RE轉換至時間自動機模型,組閤後繫統應滿足的性質用分支時序邏輯CTL公式錶示,最後應用模型檢測工具UPPAAL實現瞭Web服務組閤正確性的自動化驗證.
Web복무조합적정학성험증대제고연건개발효솔、실현복무증치구유중요의의.위종고층추상층차연구Web복무조합적정학성급기형식화험증방법,고필도Web복무조합중적실시특정,재채용연건체계결구묘술어언XYZ/ADL대Web복무조합진행묘술적기출상,장기실시묘술부분XYZ/RE전환지시간자동궤모형,조합후계통응만족적성질용분지시서라집CTL공식표시,최후응용모형검측공구UPPAAL실현료Web복무조합정학성적자동화험증.
