通信学报
通信學報
통신학보
JOURNAL OF CHINA INSTITUTE OF COMMUNICATIONS
2012年
z2期
1-8
,共8页
曹玖新%吴江林%王国进%刘波%杨鹏伟%董丹
曹玖新%吳江林%王國進%劉波%楊鵬偉%董丹
조구신%오강림%왕국진%류파%양붕위%동단
Web服务%服务组合%有限状态机%Alloy%验证
Web服務%服務組閤%有限狀態機%Alloy%驗證
Web복무%복무조합%유한상태궤%Alloy%험증
服务组合是服务计算的核心问题,而服务组合的正确性与可算性则是服务正确执行的前提保证.首先提出一种基于Alloy的服务组合验证方法,采用有限的状态机建模WS-BPEL业务流程的状态变迁,利用Alloy语言对待验证的属性进行描述,通过Alloy模型完成有限状态机的形式化,最后使用AlloyAnalyzer分析组合服务是否满足验证属性要求.实验研究表明,所提出的基于Alloy的服务组合验证方法具有较好的可行性.
服務組閤是服務計算的覈心問題,而服務組閤的正確性與可算性則是服務正確執行的前提保證.首先提齣一種基于Alloy的服務組閤驗證方法,採用有限的狀態機建模WS-BPEL業務流程的狀態變遷,利用Alloy語言對待驗證的屬性進行描述,通過Alloy模型完成有限狀態機的形式化,最後使用AlloyAnalyzer分析組閤服務是否滿足驗證屬性要求.實驗研究錶明,所提齣的基于Alloy的服務組閤驗證方法具有較好的可行性.
복무조합시복무계산적핵심문제,이복무조합적정학성여가산성칙시복무정학집행적전제보증.수선제출일충기우Alloy적복무조합험증방법,채용유한적상태궤건모WS-BPEL업무류정적상태변천,이용Alloy어언대대험증적속성진행묘술,통과Alloy모형완성유한상태궤적형식화,최후사용AlloyAnalyzer분석조합복무시부만족험증속성요구.실험연구표명,소제출적기우Alloy적복무조합험증방법구유교호적가행성.
