基于模型检测的服务规则路由正确性验证方法

留言板

尊敬的读者、作者、审稿人, 关于本刊的投稿、审稿、编辑和出版的任何问题, 您可以本页添加留言。我们将尽快给您答复。谢谢您的支持!

姓名
邮箱
手机号码
标题
留言内容
验证码

基于模型检测的服务规则路由正确性验证方法

俞东进, 吴为, 殷昱煜, 闫大强, 刘志清

文章导航 > 电子科技大学学报 > 2014 > 43(1): 107-112

俞东进, 吴为, 殷昱煜, 闫大强, 刘志清. 基于模型检测的服务规则路由正确性验证方法[J]. 电子科技大学学报, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

引用本文:

俞东进, 吴为, 殷昱煜, 闫大强, 刘志清. 基于模型检测的服务规则路由正确性验证方法[J]. 电子科技大学学报, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

YU Dong-jin, WU Wei, YIN Yu-yu, YAN Da-qiang, LIU Zhi-qing. Verification of Rule-Based Service Routing Via Model Checking[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

Citation:

YU Dong-jin, WU Wei, YIN Yu-yu, YAN Da-qiang, LIU Zhi-qing. Verification of Rule-Based Service Routing Via Model Checking[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

基于模型检测的服务规则路由正确性验证方法

doi: 10.3969/j.issn.1001-0548.2014.01.018

1.
杭州电子科技大学计算机学院杭州 310018;
2.
浙江省网络系统及信息安全重点实验室杭州 310006

基金项目:

国家自然科学基金(61100043);浙江省自然科学基金(LY12F02003);浙江省重大科技计划(2008C11099-1);浙江省网络系统及信息安全重点实验室基金

作者简介:
俞东进(1969-),男,博士,教授级高工,主要从事服务计算方面的研究.

中图分类号: TP311

Verification of Rule-Based Service Routing Via Model Checking

1.
Shool of Computer,Hangzhou Dianzi University Hangzhou 310018;
2.
Zhejiang Key Laboratory of Network System and Information Security Hangzhou 310006

摘要: 基于模型检测技术,提出了一种适用于集成了规则引擎的企业服务总线中的消息规则路由的正确性验证方法。首先将基于规则的消息路由转换为服务模型六元组,然后再将服务模型六元组转换为NuSMV输入程序,最后通过NuSMV工具实现自动化验证。给出了一个贷款审批业务的服务规则。路由的正确性验证实例证明了该方法的可行性。
- 正确性验证 /
- 企业服务总线 /
- 消息路由 /
- 模型检测 /
- 规则引擎
Abstract: To separate the business rules from corresponding processes in the traditional enterpriseservice- bus (ESB) based applications could lead to the lower maintenance cost. However, with the increasing business complexities, the correctness of rule-based service composition is often hard to be verified. This paper presents a novel model checking approach to verify the correctness of rule-based message routing in ESB integrated with rule engine. First, the message routing rules are converted into the six-tuple service model which is then transformed into the input program of NuSMV. The automatic verification is finally achieved with the help of NuSMV. The example demonstrates how to verify the correctness of rule-based message routing of loan approval service and proves the feasibility of this approach.
- correctness verification /
- enterprise service bus /
- message routing /
- model checking /
- rule engine

[1]	刘燕群, 熊蓉, 肖婷, 杨燕, 刘康, 冯刚, 宋桂芹. 肝癌转移相关基因预后模型的建立与验证 . 电子科技大学学报, 2022, 51(2): 184-193. doi: 10.12178/1001-0548.2021301
[2]	杨帆, 杨国武, 郝玉洁. 基于模型检测的半量子密码协议的安全性分析 . 电子科技大学学报, 2017, 46(5): 716-721. doi: 10.3969/j.issn.1001-0548.2017.05.013
[3]	邓达, 徐鹏. 基于优先级的WMSN区分服务路由算法 . 电子科技大学学报, 2016, 45(3): 423-428. doi: 10.3969/j.issn.1001-0548.2016.02.019
[4]	张涛, 谢红, 黄少滨. 多Agent交互策略模型检测方法 . 电子科技大学学报, 2016, 45(5): 802-807. doi: 10.3969/j.issn.1001-0548.2016.05.016
[5]	聂旭云, 杨炎, 刘梦娟, 秦志光. 基于节点能力模型的容迟网络路由算法 . 电子科技大学学报, 2013, 42(6): 905-910. doi: 10.3969/j.issn.1001-0548.2013.06.018
[6]	吴丹, 危胜军. 基于模型检测的策略冲突检测方法 . 电子科技大学学报, 2013, 42(5): 745-748,768. doi: 10.3969/j.issn.1001-0548.2013.05.019
[7]	彭云峰, 何模雄, 隆克平. 入侵检测灰色空间模型及应用 . 电子科技大学学报, 2012, 41(3): 453-458. doi: 10.3969/j.issn.1001-0548.2012.03.025
[8]	罗谦, 唐常杰, 郑皎凌, 胡建. 基于多槽分桶的快速规则冲突检测算法 . 电子科技大学学报, 2012, 41(3): 447-452. doi: 10.3969/j.issn.1001-0548.2012.03.024
[9]	朱怡安, 雷万保. 基于服务关联模型的服务排序算法——ServiceRank . 电子科技大学学报, 2011, 40(4): 607-611. doi: 10.3969/j.issn.1001-0548.2011.04.027
[10]	于海征, 马建峰, 边红. 容忍延迟网络中基于生灭模型的消息控制方法 . 电子科技大学学报, 2011, 40(1): 90-94. doi: 10.3969/j.issn.1001-0548.2011.01.017
[11]	朱维军, 邓淼磊, 周清雷, 张海宾. 扩展命题区间时序逻辑公式可满足性判定算法 . 电子科技大学学报, 2011, 40(5): 753-758. doi: 10.3969/j.issn.1001-0548.2011.05.023
[12]	桑楠, 苏芮, 廖勇, 黄小红, 侯炜, 李波. 功能性能分离的可信服务构件模型 . 电子科技大学学报, 2010, 39(2): 236-241. doi: 10.3969/j.issn.1001-0548.2010.02.018
[13]	付茂洺, 王悠. 可视化UML模型验证环境研究 . 电子科技大学学报, 2010, 39(2): 289-292,270. doi: 10.3969/j.issn.1001-0548.2010.02.029
[14]	杨世平, 李祥. 一种基于ECC的消息安全交换方案 . 电子科技大学学报, 2007, 36(5): 821-823,947.
[15]	孙朝苑, 帅斌, 陈旭. 一类基于物流服务水平的企业最优物流成本策略 . 电子科技大学学报, 2007, 36(2): 318-321.
[16]	张金林, 沈绪榜, 陈朝阳. SoC中IP核间互联总线完整性故障测试模型 . 电子科技大学学报, 2007, 36(3): 611-613,631.
[17]	唐雨虹, 曾勇, 唐小我. 量价配合的技术分析交易规则有效性研究 . 电子科技大学学报, 2005, 34(5): 720-723.
[18]	赵瑾, 庄万玉. 国内制造企业敏捷性评价模型的改进 . 电子科技大学学报, 2005, 34(3): 425-428.
[19]	梁建武, 陈语林. Internet路由器实时性的研究 . 电子科技大学学报, 2003, 32(4): 430-432,450.
[20]	唐小我, 刘莉. 支配型企业的价格领导模型研究 . 电子科技大学学报, 2000, 29(6): 640-646.

WeChat

点击查看大图

计量

文章访问数: 4250
HTML全文浏览量: 122
PDF下载量: 98
被引次数: 0

基于模型检测的服务规则路由正确性验证方法

doi: 10.3969/j.issn.1001-0548.2014.01.018

1. 杭州电子科技大学计算机学院杭州 310018;

2. 浙江省网络系统及信息安全重点实验室杭州 310006

基金项目:

国家自然科学基金(61100043);浙江省自然科学基金(LY12F02003);浙江省重大科技计划(2008C11099-1);浙江省网络系统及信息安全重点实验室基金

作者简介:
俞东进(1969-),男,博士,教授级高工,主要从事服务计算方面的研究.

收稿日期: 2012-10-22
修回日期: 2013-05-16
刊出日期: 2014-02-15

中图分类号: TP311

关键词:

摘要: 基于模型检测技术,提出了一种适用于集成了规则引擎的企业服务总线中的消息规则路由的正确性验证方法。首先将基于规则的消息路由转换为服务模型六元组,然后再将服务模型六元组转换为NuSMV输入程序,最后通过NuSMV工具实现自动化验证。给出了一个贷款审批业务的服务规则。路由的正确性验证实例证明了该方法的可行性。

English Abstract

俞东进, 吴为, 殷昱煜, 闫大强, 刘志清. 基于模型检测的服务规则路由正确性验证方法[J]. 电子科技大学学报, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

引用本文:

俞东进, 吴为, 殷昱煜, 闫大强, 刘志清. 基于模型检测的服务规则路由正确性验证方法[J]. 电子科技大学学报, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

YU Dong-jin, WU Wei, YIN Yu-yu, YAN Da-qiang, LIU Zhi-qing. Verification of Rule-Based Service Routing Via Model Checking[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

Citation:

YU Dong-jin, WU Wei, YIN Yu-yu, YAN Da-qiang, LIU Zhi-qing. Verification of Rule-Based Service Routing Via Model Checking[J]. Journal of University of Electronic Science and Technology of China, 2014, 43(1): 107-112. doi: 10.3969/j.issn.1001-0548.2014.01.018

全文HTML

/

下载: 全尺寸图片幻灯片

分享

用微信扫码二维码

分享至好友和朋友圈

返回

期刊在线

编辑办公

友情链接

电子科技大学

版权所有 © 《电子科技大学学报》编辑部

地址: 成都市建设北路二段四号电子科技大学主楼中350室电话: 028-83202308,83207559 Email: xuebao@uestc.edu.cn

本系统由北京仁和汇智信息技术有限公司开发