With the growing complexity of e-business applications and the urgent need for ensuring its reliability, much effort has been made to advocate the application of model checking in probing hidden flaws in these applications. This work devotes itself to the performance enhancement in reasoning e-business processes with model checking. Our major contribution lies in: (1) a set of business bug patterns are extracted from workflow patterns to exploit existing business knowledge in probing undesired violations in e-business processes; (2) the semantics of business bug patterns are formally captured with the IEEE standard of PSL; (3) guided verification algorithms are development based on the above findings to accelerate the reasoning of complex e-business applications. Their efficiencies are testified with three concrete business cases in banking and manufacturing domains with our business process verification toolkit of OPAL
展开▼
