Artifact systems with data dependencies and arithmetic

ABSTRACT

We revisit the static verification problem for data centric business processes, specified in a variant of IBM's "business artifact" model. Artifacts are records of variables that correspond to business-relevant objects and are updated by a set of services equipped with pre-and-post conditions, that implement business process tasks. The verification problem consists in statically checking whether all runs of an artifact system satisfy desirable properties expressed in a firstorder extension of linear-time temporal logic. In previous work we identified the class of guarded artifact systems and properties, for which verification is decidable. However, the results suffer from an important limitation: they fail in the presence of even very simple data dependencies or arithmetic, both crucial to real-life business processes. In this paper, we extend the artifact model and verification results to alleviate this limitation. We identify a practically significant class of business artifacts with data dependencies and arithmetic, for which verification is decidable. The technical machinery needed to establish the results is fundamentally different from our previous work. While the worst-case complexity of verification is non-elementary, we identify various realistic restrictions yielding more palatable upper bounds.

References

1. S. Abiteboul, V. Vianu, B. S. Fordham, and Y. Yesha. Relational transducers for electronic commerce. JCSS, 61(2):236--269, 2000. Extended abstract in PODS 98.
2. Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison Wesley, 1995.
3. Serge Abiteboul, Luc Segoufin, and Victor Vianu. Static analysis of active xml systems. ACM Trans. Database Syst., 34(4), 2009.
4. K. Bhattacharya, N. S. Caswell, S. Kumaran, A. Nigam, and F. Y. Wu. Artifact-centered operational modeling: Lessons from customer engagements. IBM Systems Journal, 46(4):703--721, 2007.
5. K. Bhattacharya et al. A model-driven approach to industrializing discovery processes in pharmaceutical research. IBM Systems Journal, 44(1):145--162, 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), 2007.
7. Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David. Two-variable logic on words with data. In LICS, pages 7--16, 2006.
8. A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu. Rewriting systems with data. In FCT'07, volume 4639 of Lecture Notes in Computer Science, pages 1--22. Springer, 2007.
9. A. Bouajjani, P. Habermehl, and R. Mayr. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science, 295:85--106, 2003.
10. 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.
11. P. Bouyer. A logical characterization of data languages. Information Processing Letters, 84(2):75--85, 2002.
12. P. Bouyer, A. Petit, and D. Thérien. An algebraic approach to data languages and timed languages. Information and Computation, 182(2):137--162, 2003.
13. O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification of infinite structures. In Handbook of Process Algebra, pages 545--623. Elsevier Science, 2001.
14. Diego Calvanese, Giuseppe De Giacomo, Richard Hull, and Jianwen Su. Artifact-centric workflow dominance. In ICSOC/ServiceWave, pages 130--143, 2009.
15. Stéphane Demri and Ranko Lazić. LTL with the Freeze Quantifier and Register Automata. In LICS, pages 17--26, 2006.
16. Stéphane Demri, Ranko Lazić, and Arnaud 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), 2008.
17. Alin Deutsch, Richard Hull, Fabio Patrizi, and Victor Vianu. Automatic verification of data-centric business processes. In ICDT, pages 252--267, 2009.
18. Alin Deutsch, Alan Nash, and Jeffrey B. Remmel. The chase revisited. In PODS, pages 149--158, 2008.
19. Alin Deutsch, Liying Sui, and Victor Vianu. Specification and verification of data-driven web applications. JCSS, 73(3):442--474, 2007.
20. G. Dong, R. Hull, B. Kumar, J Su, and G Zhou. A framework for optimizing distributed workflow executions. In Proc. Intl. Workshop on Database Programming Languages (DBPL), pages 152--167, 1999.
21. R. Hull et al. Introducing the guard-stage-milestone approach for specifying business entity lifecycles. In Proc. of 7th Intl. Workshop on Web Services and Formal Methods (WS-FM), 2010. To appear.
22. Ronald Fagin. Horn clauses and database dependencies. J. ACM, 29(4):952--985, 1982.
23. Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, and Lucian Popa. Data exchange: Semantics and query answering. In ICDT, pages 207--224, 2003.
24. C. E. Gerede, K. Bhattacharya, and J. Su. Static analysis of business artifact-centric operational models. In IEEE International Conference on Service-Oriented Computing and Applications, 2007.
25. C. E. Gerede and J. Su. Specification and verification of artifact behaviors in business process models. In Proceedings of 5th International Conference on Service-Oriented Computing (ICSOC), Vienna, Austria, September 2007.
26. R. J. Glushko and T. McGrath. Document Engineering: Analyzing and Designing Documents for Business Informatics and Web Services. MIT Press, Cmabridge, MA, 2005.
27. R. Hull, F. Llirbat, B. Kumar, G. Zhou, G. Dong, and J. Su. Optimization techniques for data-intensive decision flows. In Proc. IEEE Intl. Conf. on Data Engineering (ICDE), pages 281--292, 2000.
28. R. Hull, F. Llirbat, E. Simon, J. Su, G. Dong, B. Kumar, and G. Zhou. Declarative workflows that support easy modification and dynamic browsing. In Proc. Int. Joint Conf. on Work Activities Coordination and Collaboration, 1999.
29. Marcin Jurdzinski and Ranko Lazić. Alternation-free modal mu-calculus for data trees. In LICS, pages 131--140, 2007.
30. N. Karmarkar. A new polynomial-time algorithm for linear programming. In STOC, pages 302--311, 1984.
31. S. Kumaran, R. Liu, and F. Y. Wu. On the duality of information-centric and activity-centric models of business processes. In Proc. Intl. Conf. on Advanced Information Systems Engineering (CAISE), 2008.
32. S. Kumaran, P. Nandi, T. Heath, K. Bhaskaran, and R. Das. A Doc-oriented programming. In Symp. on Applications and the Internet (SAINT), pages 334--343, 2003.
33. 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.
34. R. Lazić, Th. 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.
35. Leonid Libkin. Elements of Finite Model Theory. Springer, 2004.
36. R. Liu, K. Bhattacharya, and F. Y. Wu. Modeling business contexture and behavior using business artifacts. In CAiSE, volume 4495 of LNCS, 2007.
37. D. Martin et al. OWL-S: Semantic markup for web services, W3C Member Submission, November 2003.
38. S. A. McIlraith, T. C. Son, and H. Zeng. Semantic web services. IEEE Intelligent Systems, 16(2):46--53, 2001.
39. Michael Meier, Michael Schmidt, Fang Wei, and Georg Lausen. Semantic query optimization in the presence of types. In PODS, pages 111--122, 2010.
40. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1967.
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. S. Narayanan and S. McIlraith. Simulation, verification and automated composition of web services. In Intl. World Wide Web Conf. (WWW2002), 2002.
43. F. Neven, T. Schwentick, and V. Vianu. Finite State Machines for Strings Over Infinite Alphabets. ACM Transactions on Computational Logic, 5(3):403--435, 2004.
44. A. Nigam and N. S. Caswell. Business artifacts: An approach to operational specification. IBM Systems Journal, 42(3):428--445, 2003.
45. Amir Pnueli. The temporal logic of programs. In FOCS, pages 46--57, 1977.
46. M. Spielmann. Verification of relational transducers for electronic commerce. JCSS., 66(1):40--65, 2003. Extended abstract in PODS 2000.
47. J. Wang and A. Kumar. A framework for document-driven workflow systems. In Business Process Management, pages 285--301, 2005.
48. Xiangpeng Zhao, Jianwen Su, Hongli Yang, and Zongyan Qiu. Enforcing constraints on life cycles of business artifacts. In TASE, pages 111--118, 2009.

Index Terms

• Applied computing

  • Enterprise computing

    • Enterprise information systems

      • Enterprise applications

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Information systems

  • Information systems applications

    • Enterprise information systems

      • Enterprise applications

• Social and professional topics

  • Professional topics

    • Computing and business

      • Automation

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software notations and tools

    • General programming languages

      • Language types

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification