CAJ | 학술논문

近几年Web服务组合的形式化验证逐渐成为研究热点.模型检测作为形式化验证的一种主流技术,可以克服传统软件测试用例生成不完备的不足,同时具有验证自动化的优点.该文提出并实现了一种Web服务组合的认知模型检测方法,将Web服务组合建模为多主体系统,在分析BPEL语言控制流程基础上,提出BPEL活动的形式化模型,给出活动执行语义.进而以迁移七元组为中间形式,开发从BPEL流程到迁移七元组集合以及从这些迁移七元组到MCTK(一种我们开发的多主体系统模型检测工具)输入语言的自动转换算法,最终通过MCTK进行验证.实验结果表明开发的算法不仅可以有效验证Web服务组合的时态逻辑规范,而且可以验证多主体系统特有的认知逻辑规范及其时态组合.
근궤년Web복무조합적형식화험증축점성위연구열점.모형검측작위형식화험증적일충주류기술,가이극복전통연건측시용례생성불완비적불족,동시구유험증자동화적우점.해문제출병실현료일충Web복무조합적인지모형검측방법,장Web복무조합건모위다주체계통,재분석BPEL어언공제류정기출상,제출BPEL활동적형식화모형,급출활동집행어의.진이이천이칠원조위중간형식,개발종BPEL류정도천이칠원조집합이급종저사천이칠원조도MCTK(일충아문개발적다주체계통모형검측공구)수입어언적자동전환산법,최종통과MCTK진행험증.실험결과표명개발적산법불부가이유효험증Web복무조합적시태라집규범,이차가이험증다주체계통특유적인지라집규범급기시태조합.