Verification of Business Processes Against Business Rules Using Object Life Cycles

While formal verification of business process models (BPMs) can be done through model checking (also known as property checking), formalizing corresponding properties having the process model available may negatively influence the formulation of properties to be checked. In addition, properties should be checkable for several processes. So, we address the problem of formalizing properties without knowing the process model. The solution proposed in this paper employs additional models of object life cycles. The new key idea is to formulate properties referring to these additional models, which together can represent certain business rules. These models have to be connected with the BPM to be checked in the formalism used for model checking. This combination facilitates more rigorous model checking with a better decoupling of the specification of the original BPM from the properties to be checked. In summary, this paper presents how a combination of conventional business process models (given, e.g., in BPMN), models of business object life cycles, and formalized business rules can be used for verification through model checking.