Automatic verification of data-centric business processes

ABSTRACT

We formalize and study business process systems that are centered around "business artifacts", or simply "artifacts". Artifacts are used to represent (real or conceptual) key business entities, including both their data schema and lifecycles. The lifecycle of an artifact type specifies the possible sequencings of services that can be applied to an artifact of this type as it progresses through the business process. The artifact-centric approach was introduced by IBM, and has been used to achieve substantial savings when performing business transformations.

In this paper, artifacts carry attribute records and internal state relations (holding sets of tuples) that services can consult and update. In addition, services can access an underlying database and can introduce new values from an infinite domain, thus modeling external inputs or partially specified processes described by pre-and-post conditions. The lifecycles associate services to the artifacts using declarative, condition-action style rules.

We consider the problem of statically verifying whether all runs of an artifact system satisfy desirable correctness properties expressed in a first-order extension of linear-time temporal logic. We map the boundaries of decidability for the verification problem and provide its complexity. The technical challenge to static verification stems from the presence of data from an infinite domain, yielding an infinite-state system. While much work has been done lately in the verification community on model checking specialized classes of infinite-state systems, the available results do not transfer to our framework, and this remains a difficult problem. We identify an expressive class of artifact systems for which verification is nonetheless decidable. The complexity of verification is PSPACE-complete, which is no worse than classical finite-state model checking.

This investigation builds upon previous work on verification of data-driven Web services and ASM transducers, while addressing significant new technical challenges raised by the artifact model.

REFERENCES

• 1: Serge Abiteboul , Laurent Herr , Jan Van den Bussche, Temporal versus first-order logic to query temporal databases, Proceedings of the fifteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.49-57, June 04-06, 1996, Montreal, Quebec, Canada [doi>10.1145/237661.237674]
• 2: Serge Abiteboul , Luc Segoufin , Victor Vianu, Static analysis of active XML systems, Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 09-12, 2008, Vancouver, Canada [doi>10.1145/1376916.1376948]
• 3: Serge Abiteboul , Victor Vianu , Brad Fordham , Yelena Yesha, Relational transducers for electronic commerce, Journal of Computer and System Sciences, v.61 n.2, p.236-269, Oct. 2000 [doi>10.1006/jcss.2000.1708]
• 4: K. Bhattacharya , N. S. Caswell , S. Kumaran , A. Nigam , F. Y. Wu, Artifact-centered operational modeling: lessons from customer engagements, IBM Systems Journal, v.46 n.4, p.703-721, October 2007
• 5: K. Bhattacharya , R. Guthman , K. Lyman , F. F. Heath, III , S. Kumaran , P. Nandi , F. Wu , P. Athma , C. Freiberg , L. Johannsen , A. Staudt, A model-driven approach to industrializing discovery processes in pharmaceutical research, IBM Systems Journal, v.44 n.1, p.145-162, January 2005
• 6: K. Bhattacharya, C. E. Gerede, R. Hull, R. Liu, and J. Su. Towards formal analysis of artifact-centric business process models. In Proc. Int. Conf. on Business Process Management (BPM), pages 288--304, 2007.
• 7: K. Bhattacharya, R. Hull, and J. Su. A Data-centric Design Methodology for Business Processes. In J. Cardoso and W. van der Aalst, editors, Handbook of Research on Business Process Management. 2009. to appear.
• 8: Mikolaj Bojanczyk , Anca Muscholl , Thomas Schwentick , Luc Segoufin , Claire David, Two-Variable Logic on Words with Data, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.7-16, August 12-15, 2006 [doi>10.1109/LICS.2006.51]
• 9: E. Borger, E. Gradel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997.
• 10: Ahmed Bouajjani , Peter Habermehl , Yan Jurski , Mihaela Sighireanu, Rewriting Systems with Data, Proceedings of the 16th international symposium on Fundamentals of Computation Theory, August 27-30, 2007, Budapest, Hungary [doi>10.1007/978-3-540-74240-1_1]
• 11: Ahmed Bouajjani , Peter Habermehl , Richard Mayr, Automatic verification of recursive procedures with one integer parameter, Theoretical Computer Science, v.295 n.1-3, p.85-106, 24 February 2003 [doi>10.1016/S0304-3975(02)00397-3]
• 12: A. Bouajjani, Y. Jurski, and M. Sighireanu. A generic framework for reasoning about dynamic networks of infinite-state processes. In TACAS'07, volume 4424 of Lecture Notes in Computer Science, pages 690--705. Springer, 2007.
• 13: Patricia Bouyer, A logical characterization of data languages, Information Processing Letters, v.84 n.2, p.75-85, 31 October 2002 [doi>10.1016/S0020-0190(02)00229-6]
• 14: Patricia Bouyer , Antoine Petit , Denis Thérien, An algebraic approach to data languages and timed languages, Information and Computation, v.182 n.2, p.137-162, 01 May 2003 [doi>10.1016/S0890-5401(03)00038-5]
• 15: O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification of infinite structures. In Handbook of Process Algebra, pages 545--623. Elsevier Science, 2001.
• 16: A. K. Chandra and M. Vardi. The implication problem for functional and inclusion dependencies is undecidable. SIAM J. Comp., 14(3):671--677, 1985.
• 17: David Cohn , Pankaj Dhoolia , Fenno Heath, Iii , Florian Pinel , John Vergo, Siena: From PowerPoint to Web App in 5 Minutes, Proceedings of the 6th International Conference on Service-Oriented Computing, p.722-723, December 01-05, 2008, Sydney, Australia [doi>10.1007/978-3-540-89652-4_63]
• 18: Stephane Demri , Ranko Lazic, LTL with the Freeze Quantifier and Register Automata, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.17-26, August 12-15, 2006 [doi>10.1109/LICS.2006.31]
• 19: S. Demri, R. Lazić, and A. Sangnier. Model checking freeze LTL over one-counter automata. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08), pages 490--504, 2008.
• 20: Alin Deutsch , Monica Marcus , Liying Sui , Victor Vianu , Dayou Zhou, A verifier for interactive, data-driven web applications, Proceedings of the 2005 ACM SIGMOD international conference on Management of data, June 14-16, 2005, Baltimore, Maryland [doi>10.1145/1066157.1066219]
• 21: Alin Deutsch , Liying Sui , Victor Vianu, Specification and verification of data-driven Web applications, Journal of Computer and System Sciences, v.73 n.3, p.442-474, May, 2007 [doi>10.1016/j.jcss.2006.10.006]
• 22: Alin Deutsch , Liying Sui , Victor Vianu , Dayou Zhou, A system for specification and verification of interactive, data-driven web applications, Proceedings of the 2006 ACM SIGMOD international conference on Management of data, June 27-29, 2006, Chicago, IL, USA [doi>10.1145/1142473.1142584]
• 23: Alin Deutsch , Liying Sui , Victor Vianu , Dayou Zhou, Verification of communicating data-driven web services, Proceedings of the twenty-fifth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 26-28, 2006, Chicago, IL, USA [doi>10.1145/1142351.1142364]
• 24: Guozhu Dong , Richard Hull , Bharat Kumar , Jianwen Su , Gang Zhou, A Framework for Optimizing Distributed Workflow Executions, Revised Papers from the 7th International Workshop on Database Programming Languages: Research Issues in Structured and Semistructured Database Programming, p.152-167, September 01-03, 1999
• 25: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 26: Christian Fritz , Richard Hull , Jianwen Su, Automatic construction of simple artifact-based business processes, Proceedings of the 12th International Conference on Database Theory, March 23-25, 2009, St. Petersburg, Russia [doi>10.1145/1514894.1514922]
• 27: Cagdas E. Gerede , Kamal Bhattacharya , Jianwen Su, Static Analysis of Business Artifact-centric Operational Models, Proceedings of the IEEE International Conference on Service-Oriented Computing and Applications, p.133-140, June 19-20, 2007 [doi>10.1109/SOCA.2007.42]
• 28: Cagdas E. Gerede , Jianwen Su, Specification and Verification of Artifact Behaviors in Business Process Models, Proceedings of the 5th international conference on Service-Oriented Computing, September 17-20, 2007, Vienna, Austria [doi>10.1007/978-3-540-74974-5_15]
• 29: R. Glushko and T. McGrath. Document Engineering: Analyzing and Designing Documents for Business Infomratics and Web Services. MIT Press, Cmabridge, MA, 2005.
• 30: Richard Hull, Artifact-Centric Business Process Models: Brief Survey of Research Results and Challenges, Proceedings of the OTM 2008 Confederated International Conferences, CoopIS, DOA, GADA, IS, and ODBASE 2008. Part II on On the Move to Meaningful Internet Systems, November 09-17, 2008, Monterrey, Mexico [doi>10.1007/978-3-540-88873-4_17]
• 31: Optimization Techniques for Data-Intensive Decision Flows, Proceedings of the 16th International Conference on Data Engineering, p.281, February 28-March 03, 2000
• 32: Richard Hull , Francois Llirbat , Eric Siman , Jianwen Su , Guozhu Dong , Bharat Kumar , Gang Zhou, Declarative workflows that support easy modification and dynamic browsing, Proceedings of the international joint conference on Work activities coordination and collaboration, p.69-78, February 22-25, 1999, San Francisco, California, United States
• 33: Marcin Jurdzinski , Ranko Lazic, Alternation-free modal mu-calculus for data trees, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.131-140, July 10-14, 2007 [doi>10.1109/LICS.2007.11]
• 34: Santhosh Kumaran , Rong Liu , Frederick Y. Wu, On the Duality of Information-Centric and Activity-Centric Models of Business Processes, Proceedings of the 20th international conference on Advanced Information Systems Engineering, June 16-20, 2008 [doi>10.1007/978-3-540-69534-9_3]
• 35: Santhosh Kumaran , Prabir Nandi , Terry Heath , Kumar Bhaskaran , Raja Das, ADoc-Oriented Programming, Proceedings of the 2003 Symposium on Applications and the Internet, p.334, January 27-31, 2003
• 36: J. Küster, K. Ryndina, and H. Gall. Generation of BPM for object life cycle compliance. In Proceedings of 5th International Conference on Business Process Management (BPM), 2007.
• 37: R. Lazić, T. Newcomb, J. Ouaknine, A. Roscoe, and J. Worrell. Nets with tokens which carry data. In ICATPN'07, volume 4546 of Lecture Notes in Computer Science, pages 301--320. Springer, 2007.
• 38: R. Liu, K. Bhattacharya, and F. Y. Wu. Modeling business contexture and behavior using business artifacts. In CAiSE, volume 4495 of LNCS, 2007.
• 39: D. Martin et al. OWL-S: Semantic markup for web services, W3C Member Submission, November 2003.
• 40: Sheila A. McIlraith , Tran Cao Son , Honglei Zeng, Semantic Web Services, IEEE Intelligent Systems, v.16 n.2, p.46-53, March 2001 [doi>10.1109/5254.920599]
• 41: P. Nandi and S. Kumaran. Adaptive business objects -- a new component model for business integration. In Proc. Intl. Conf. on Enterprise Information Systems, pages 179--188, 2005.
• 42: Srini Narayanan , Sheila A. McIlraith, Simulation, verification and automated composition of web services, Proceedings of the 11th international conference on World Wide Web, May 07-11, 2002, Honolulu, Hawaii, USA [doi>10.1145/511446.511457]
• 43: Frank Neven , Thomas Schwentick , Victor Vianu, Finite state machines for strings over infinite alphabets, ACM Transactions on Computational Logic (TOCL), v.5 n.3, p.403-435, July 2004 [doi>10.1145/1013560.1013562]
• 44: A. Nigam , N. S. Caswell, Business artifacts: An approach to operational specification, IBM Systems Journal, v.42 n.3, p.428-445, July 2003
• 45: M. Spielmann. Abstract State Machines: Verification problems and complexity. Ph.D. thesis, RWTH Aachen, 2000.
• 46: Marc Spielmann, Verification of relational transducers for electronic commerce, Journal of Computer and System Sciences, v.66 n.1, p.40-65, 01 February 2003 [doi>10.1016/S0022-0000(02)00029-6]
• 47: J. K. Strosnider , P. Nandi , S. Kumaran , S. Ghosh , A. Arsanjani, Model-driven synthesis of SOA solutions, IBM Systems Journal, v.47 n.3, p.415-432, July 2008
• 48: J. Wang and A. Kumar. A framework for document-driven workflow systems. In Business Process Management, pages 285--301, 2005.