基于模型检测的服务规则路由正确性验证方法
|
摘要
基于模型检测技术,提出了一种适用于集成了规则引擎的企业服务总线中的消息规则路由的正确性验证方法。首先将基于规则的消息路由转换为服务模型六元组,然后再将服务模型六元组转换为NuSMV输入程序,最后通过NuSMV工具实现自动化验证。给出了一个贷款审批业务的服务规则。路由的正确性验证实例证明了该方法的可行性。
To separate the business rules from corresponding processes in the traditional enterprise- service-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.
To separate the business rules from corresponding processes in the traditional enterprise- service-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.
引文
[1]VON RIEGEN M,HUSEMANN,FINK S,et al.Rule-based coordination of distributed Web service transactions[J].IEEE Transactions on Services Computing,2010,3(1):60-72.
[2]杨娟,曹健.基于规则的服务流程配置模型与系统[J].计算机集成制造系统,2009,15(8):1547-1554.YANG Juan,CAO Jian.Rule based service process configuration model and system[J].Computer Integrated Manufacturing Systems,2009,15(8):1547-1554.
[3]WARAWOOT P,TOSHIAKI A,ATHASIT S,et al.Conformance verification between Web service choreography and implementation using learning and model checking[C]//2011 IEEE 9th International Conference on Web Services.Hawaii,USA:IEEE,2011:722-723.
[4]SYLVAIN H,ROGER V,OMAR C.Specifying and validating data-aware temporal Web service properties[J].IEEE Transactions on Software Engineering,2009,35(5):669-683.
[5]FENG Y Z,MARKUS K.Verifying OWL-S service process models[C]//2011 IEEE 9th International Conference on Web Services.Hawaii,USA:IEEE,2011:307-314.
[6]骆翔宇,谭征,苏开乐,等.一种基于认知模型检测的Web服务组合验证方法[J].计算机学报,2011,34(6):1041-1061.LUO Xiang-yu,TAN Zheng,SU Kai-le,et al.A verification approach for Web service compositions based on epistemic model checking[J].Chinese Journal of Computers,2011,34(6):1041-1061.
[7]CLARKE E M.The birth of model checking[M].Berlin Heidelberg:Springr-Verlag,2008.
[8]王雷,陈归,金茂忠.基于约束分析与模型检测的代码安全漏洞检测方法研究[J].计算机研究与发展,2011,48(9):1659-1666.WANG Lei,CHEN Gui,JIN Mao-zhong.Detection of code vulnerabilities via constraint-based analysis and model checking[J].Journal of Computer Research and Development,2011,48(9):1659-1666.
[9]张阳,程亮.一种基于指针逻辑的代码安全属性分析方法[J].计算机学报,2009,32(6):1119-1125.ZHANG Yang,CHENG Liang.A new property verification method for code security based on pointer logic[J].Chinese Journal of Computers,2009,32(6):1119-1125.
[10]周从华.一种基于满足性判定的并发软件验证策略[J].软件学报,2009,20(6):1414-1424.ZHOU Cong-hua.SAT-based compositional verification strategy for concurrent software with states events[J].Journal of Software,2009,20(6):1414-1424.
[11]张广泉,戎玫,朱雪阳,等.基于XYZ/ADL的Web服务组合描述与验证[J].电子学报,2011,39(3):86-93.ZHANG Guang-quan,RONG Mei,ZHU Xue-yang,et al.Specification and verification of Web service composition based on XYZ/ADL[J].Acta Electronica Sinica,2011,39(3):86-93.
[12]桂盛霖,罗蕾,李允,等.基于自动机理论的分布式实时调度分析工具[J].软件学报,2011,22(6):1236-1251.GUI Sheng-lin,LUO Lei,LI Yun,et al.Schedulability analysis tool for distributed real-time systems based on automata theory[J].Journal of Software,2011,22(6):1236-1251.
[13]SCHUPPAN V,BIERE A.Liveness checking as safety checking for infinite state spaces[J].Electronic Notes in Theoretical Computer Science,2006,149(1):79-96.
[14]RAMASWAMY M,SARKAR S,YE S C.Using directed hypergraphs to verify rule-based expert systems[J].IEEE Transactions on Knowledge and Data Engineering,2007,19(2):221-237.
[15]YANG S J H,TSAI J J P,CHYUN C C.Fuzzy rule base systems verification using high-level Petri nets[J].IEEE Transactions on Knowledge and Data Engineering,2003,15(2):457-473.
[16]CHAVARRIA-BAEZ L,LI X O.Structural error verification in active rule-based systems using Petri nets[C]//Fifth Mexican International Conference on Artificial Intelligence.Mexico City:IEEE,2006:12-21.
[17]HE X D.A new approach to verify rule-based systems using Petri nets[J].Information and Software Technology,2003,45(10):462-467.
[18]YEH C W,CHU C P.Molecular verification of rule-based systems based on DNA computation[J].IEEE Transactions on Knowledge and Data Engineering,2008,20(7):965-975.
[19]MA J,LU J,ZHANG G Q.A rule-map based technique for information inconsistency verification[C]//Proceeding of2007 Information,Decision and Control.Adelaide:IEEE,2007:296-301.
[20]SHEN V R L,JUANG T T Y.Verification of knowledgebased systems using predicate/transition nets[J].IEEE Transactions on Systems,Man,and Cybernetics Part A:Systems and Humans,2008,38(1):78-87.
[21]OASIS.Web services business process execution language,version 2.0[EB/OL].[2012-06-27].http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.pdf
[2]杨娟,曹健.基于规则的服务流程配置模型与系统[J].计算机集成制造系统,2009,15(8):1547-1554.YANG Juan,CAO Jian.Rule based service process configuration model and system[J].Computer Integrated Manufacturing Systems,2009,15(8):1547-1554.
[3]WARAWOOT P,TOSHIAKI A,ATHASIT S,et al.Conformance verification between Web service choreography and implementation using learning and model checking[C]//2011 IEEE 9th International Conference on Web Services.Hawaii,USA:IEEE,2011:722-723.
[4]SYLVAIN H,ROGER V,OMAR C.Specifying and validating data-aware temporal Web service properties[J].IEEE Transactions on Software Engineering,2009,35(5):669-683.
[5]FENG Y Z,MARKUS K.Verifying OWL-S service process models[C]//2011 IEEE 9th International Conference on Web Services.Hawaii,USA:IEEE,2011:307-314.
[6]骆翔宇,谭征,苏开乐,等.一种基于认知模型检测的Web服务组合验证方法[J].计算机学报,2011,34(6):1041-1061.LUO Xiang-yu,TAN Zheng,SU Kai-le,et al.A verification approach for Web service compositions based on epistemic model checking[J].Chinese Journal of Computers,2011,34(6):1041-1061.
[7]CLARKE E M.The birth of model checking[M].Berlin Heidelberg:Springr-Verlag,2008.
[8]王雷,陈归,金茂忠.基于约束分析与模型检测的代码安全漏洞检测方法研究[J].计算机研究与发展,2011,48(9):1659-1666.WANG Lei,CHEN Gui,JIN Mao-zhong.Detection of code vulnerabilities via constraint-based analysis and model checking[J].Journal of Computer Research and Development,2011,48(9):1659-1666.
[9]张阳,程亮.一种基于指针逻辑的代码安全属性分析方法[J].计算机学报,2009,32(6):1119-1125.ZHANG Yang,CHENG Liang.A new property verification method for code security based on pointer logic[J].Chinese Journal of Computers,2009,32(6):1119-1125.
[10]周从华.一种基于满足性判定的并发软件验证策略[J].软件学报,2009,20(6):1414-1424.ZHOU Cong-hua.SAT-based compositional verification strategy for concurrent software with states events[J].Journal of Software,2009,20(6):1414-1424.
[11]张广泉,戎玫,朱雪阳,等.基于XYZ/ADL的Web服务组合描述与验证[J].电子学报,2011,39(3):86-93.ZHANG Guang-quan,RONG Mei,ZHU Xue-yang,et al.Specification and verification of Web service composition based on XYZ/ADL[J].Acta Electronica Sinica,2011,39(3):86-93.
[12]桂盛霖,罗蕾,李允,等.基于自动机理论的分布式实时调度分析工具[J].软件学报,2011,22(6):1236-1251.GUI Sheng-lin,LUO Lei,LI Yun,et al.Schedulability analysis tool for distributed real-time systems based on automata theory[J].Journal of Software,2011,22(6):1236-1251.
[13]SCHUPPAN V,BIERE A.Liveness checking as safety checking for infinite state spaces[J].Electronic Notes in Theoretical Computer Science,2006,149(1):79-96.
[14]RAMASWAMY M,SARKAR S,YE S C.Using directed hypergraphs to verify rule-based expert systems[J].IEEE Transactions on Knowledge and Data Engineering,2007,19(2):221-237.
[15]YANG S J H,TSAI J J P,CHYUN C C.Fuzzy rule base systems verification using high-level Petri nets[J].IEEE Transactions on Knowledge and Data Engineering,2003,15(2):457-473.
[16]CHAVARRIA-BAEZ L,LI X O.Structural error verification in active rule-based systems using Petri nets[C]//Fifth Mexican International Conference on Artificial Intelligence.Mexico City:IEEE,2006:12-21.
[17]HE X D.A new approach to verify rule-based systems using Petri nets[J].Information and Software Technology,2003,45(10):462-467.
[18]YEH C W,CHU C P.Molecular verification of rule-based systems based on DNA computation[J].IEEE Transactions on Knowledge and Data Engineering,2008,20(7):965-975.
[19]MA J,LU J,ZHANG G Q.A rule-map based technique for information inconsistency verification[C]//Proceeding of2007 Information,Decision and Control.Adelaide:IEEE,2007:296-301.
[20]SHEN V R L,JUANG T T Y.Verification of knowledgebased systems using predicate/transition nets[J].IEEE Transactions on Systems,Man,and Cybernetics Part A:Systems and Humans,2008,38(1):78-87.
[21]OASIS.Web services business process execution language,version 2.0[EB/OL].[2012-06-27].http://docs.oasis-open.org/wsbpel/2.0/OS/wsbpel-v2.0-OS.pdf