Verification of Business Process Constraints Based on XYZ/Z

Enterprise´s behaviors are always restricted by a number of business constraint rules. In the context of business process reengineering, it is necessary to judge whether business processes comply with these constraint rules or not. Furthermore, the verification of business constraints against business processes is a hard job in large enterprises whose business processes and constraints are both complex. In order to automate the judgment, unambiguous formal specifications are needed. However the notations for business process modeling are usually flow-oriented languages, the notational gap to the languages usually employed for business constraints, e.g., temporal logic, is significant and hard to bridge. Thus a visual constraint modeling language, namely VCML, is proposed and a research on automatic verification technology is conducted. XYZ/E is employed to formally define the semantics of VCML. VPML is employed to describe business processes and their semantics are also defined in XYZ/E. Then the method to verify business constraints is discussed. At last, an example illustrates the modeling of business process constraint.