随着企业信息化的发展,传统的软件架构已经不能满足多个应用集成的需求。面向服务架构(Service Oriented Architecture, SOA)思想的提出在一定程度上解决了这个问题。企业服务总线(Enterprise Service Bus, ESB)作为SOA架构主要的基础设施,已经成功应用在电信、金融等多个领域。然而,随着业务复杂度的逐渐增加和用户对企业信息系统需求的不断提升,很多基于ESB架构的系统开始暴露出一些不足之处。例如,在业务规则改变时需要原有系统停止提供服务,然后修改代码并重新发布,这样就加大了系统的维护成本；又如,服务组合的正确性不能明确地被验证,由此造成用户的业务需求有可能无法得到满足。为了解决以上问题,本文提出一种面向企业服务总线的规则引擎的集成、验证框架,探讨了服务总线与规则引擎的集成方法和消息规则路由的验证方法。首先,对当前企业服务总线和形式化方法进行了综述。介绍了常用的开源企业服务总线,总结了当前服务总线的研究热点；概述了形式化验证方法,重点分析了模型检测技术的方法和原理。其次,深入剖析了Mule的实现机制,包括基本组件、运行环境和应用集成模式。提出两种Mule与Drools集成的方式：Component方式和Module方式。Component方式通过在服务组件类中调用Drools代理类对消息进行断言,进而实现基于规则的消息路由；Module方式通过扩展标签和规则类实现集成。实例验证了两种集成方式的有效性。然后,分析了使用NuSMV验证消息规则路由的方法和步骤,描述了NuSMV输入语言和时序逻辑语言LTL、CTL;提出分两步进行验证消息规则路由的方法：先将规则路由配置转换为模型六元组,再将六元组转换为NuSMV输入语言。最后,阐述了规则路由配置转换为六元组、六元组转换为NuSMV输入语言的算法和过程。通过分析基于规则的消息路由机制,得到服务之间的消息传输和状态转移,基于消息变量和服务状态变量的变换情况得到最终的smv验证程序,从而实现了基于NuSMV的路由规则的正确性验证。综上所述,本文对服务总线Mule和规则引擎Drools的集成和验证进行了研究,提出Component、Module两种集成方式和一种验证算法,实例说明了本文集成方式和验证算法的可行性和有效性。