电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2011年
z1期
86-93
,共8页
张广泉%戎玫%朱雪阳%何亚丽%石慧娟
張廣泉%戎玫%硃雪暘%何亞麗%石慧娟
장엄천%융매%주설양%하아려%석혜연
Web服务组合%XYZ/ADL%XYZ/RE%时间自动机%精化检验%模型检测
Web服務組閤%XYZ/ADL%XYZ/RE%時間自動機%精化檢驗%模型檢測
Web복무조합%XYZ/ADL%XYZ/RE%시간자동궤%정화검험%모형검측
Web服务组合是当前Web服务领域的一个研究热点,目前已有一些相关的描述与验证方法,本文从软件体系结构角度研究Web服务组合描述与验证方法.基于软件体系结构描述语言XYZ/ADL和精化检验/模型检测方法,提出了一种Web服务组合的描述与验证方法.XYZ/ADL是时序逻辑语言XYZ/E的扩展,考虑到多数Web服务具有实时特征,采用XYZ/E的实时扩展语言XYZ/RE表示系统应满足的时间约束.针对Web服务组合系统,根据XYZ/RE到时间自动机的映射规则将系统描述转换为对应的时间自动机,分别采用精化检验和模型检测两种技术验证Web服务组合的正确性;最后通过两个实例分析分别阐述了上述方法的可行性和有效性.
Web服務組閤是噹前Web服務領域的一箇研究熱點,目前已有一些相關的描述與驗證方法,本文從軟件體繫結構角度研究Web服務組閤描述與驗證方法.基于軟件體繫結構描述語言XYZ/ADL和精化檢驗/模型檢測方法,提齣瞭一種Web服務組閤的描述與驗證方法.XYZ/ADL是時序邏輯語言XYZ/E的擴展,攷慮到多數Web服務具有實時特徵,採用XYZ/E的實時擴展語言XYZ/RE錶示繫統應滿足的時間約束.針對Web服務組閤繫統,根據XYZ/RE到時間自動機的映射規則將繫統描述轉換為對應的時間自動機,分彆採用精化檢驗和模型檢測兩種技術驗證Web服務組閤的正確性;最後通過兩箇實例分析分彆闡述瞭上述方法的可行性和有效性.
Web복무조합시당전Web복무영역적일개연구열점,목전이유일사상관적묘술여험증방법,본문종연건체계결구각도연구Web복무조합묘술여험증방법.기우연건체계결구묘술어언XYZ/ADL화정화검험/모형검측방법,제출료일충Web복무조합적묘술여험증방법.XYZ/ADL시시서라집어언XYZ/E적확전,고필도다수Web복무구유실시특정,채용XYZ/E적실시확전어언XYZ/RE표시계통응만족적시간약속.침대Web복무조합계통,근거XYZ/RE도시간자동궤적영사규칙장계통묘술전환위대응적시간자동궤,분별채용정화검험화모형검측량충기술험증Web복무조합적정학성;최후통과량개실례분석분별천술료상술방법적가행성화유효성.
