-
题名基于MAS模型检测与抽象的Web服务验证
被引量：1
- 1
-
-
作者
许兴旺
骆翔宇
-
机构
华侨大学计算机科学与技术学院
桂林电子科技大学广西可信软件重点实验室
-
出处
《计算机工程》
CAS
CSCD
北大核心
2015年第3期26-31,36,共7页
-
基金
国家自然科学基金资助面上项目(61170028)
华侨大学中青年教师科研提升计划基金资助项目(ZQN-YX109)
+1 种基金
华侨大学高层次人才科研启动基金资助项目(11BS108)
广西可信软件重点实验室基金资助项目(kx201323)
-
文摘
Web服务组合现已成为跨组织业务流程集成的关键技术,然而在松耦合开发模式和开放的互联网运行环境下,其正确性、可靠性、安全性等可信性质难以得到保证。为解决该问题,提出一种Web服务组合形式化验证方法,将基于图状反例向导的抽象与精化方法应用于多主体系统(MAS)模型检测工具(MCTK)中,大幅缓解模型检测的状态爆炸问题,从理论上证明该验证方法的正确性。实验通过将银行贷款风险评估系统转换成MCTK描述的MAS,并对比抽象前后的模型检测代价,结果显示,基于抽象的Web服务验证方法明显优于未采用抽象技术的验证方法。
-
关键词
WEB服务组合
多主体系统
模型检测
图状反例
抽象
精化
-
Keywords
Web services composition
Multi-Agent System（MAS）
model checking
graph-like counterexample
abstraction
refinement
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
