With the growing complexity of e-business applications and the urgent need for ensuring its reliability and trustworthiness, 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, which is a critical issue for making the reasoning of complex e-business applications more realistically applicable. 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 enhance the performance of reasoning 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.
By: Ke Xu, Ying Liu, Cheng Wu
Published in: RC23948 in 2006
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .