Verification of Rule-Based Service Routing Via Model Checking

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.