- Web Ratio. http://www.webratio.com/.Google Scholar
- S. Abiteboul and V. Vianu. Collaborative data-driven workflows: think global, act local. In PODS, 2013. Google ScholarDigital Library
- S. Abiteboul, V. Vianu, B. Fordham, and Y. Yesha. Relational transducers for electronic commerce. JCSS, 61(2):236--269, 2000. Google ScholarDigital Library
- B.B. Hariri, D. Calvanese, G. D. Giacomo, R. D. Masellis, and P. Felli. Foundations of relational artifacts verification. In BPM, 2011. Google ScholarDigital Library
- F. Belardinelli, A. Lomuscio, and F. Patrizi. Verification of gsm-based artifact-centric systems through finite abstraction. In ICSOC, 2012. Google ScholarDigital Library
- K. Bhattacharya, N. S. Caswell, S. Kumaran, A. Nigam, and F. Y. Wu. Artifact-centered operational modeling: Lessons from customer engagements. IBM Sys. Journal, 46(4), 2007. Google ScholarDigital Library
- K. Bhattacharya et al. A model-driven approach to industrializing discovery processes in pharmaceutical research. IBM Systems Journal, 44(1), 2005. Google ScholarDigital Library
- K. Bhattacharya, C. E. Gerede, R. Hull, R. Liu, and J. Su. Towards formal analysis of artifact-centric business process models. In BPM, 2007. Google ScholarDigital Library
- BizAgi and Cordys and IBM and Oracle and SAP AG and Singularity (OMG Submitters) and Agile Enterprise Design and Stiftelsen SINTEF and TIBCO and Trisotech (Co-Authors). Case Management Model and Notation (CMMN), FTF Beta 1, Jan. 2013. OMG Document Number dtc/2013-01-01, Object Management Group.Google Scholar
- D. Boaz, L. Limonad, and M. Gupta. BizArtifact: Artifact-centric Business Process Management, June 2013. http://sourceforge.net/projects/bizartifact/.Google Scholar
- M. Bojanczyk, A. Muscholl, T. Schwentick, L. Segoufin, and C. David. Two-variable logic on words with data. In LICS, 2006. Google ScholarDigital Library
- A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu. Rewriting systems with data. In FCT'07. Google ScholarDigital Library
- A. Bouajjani, P. Habermehl, and R. Mayr. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science, 295:85--106, 2003. Google ScholarDigital Library
- A. Bouajjani, Y. Jurski, and M. Sighireanu. A generic framework for reasoning about dynamic networks of infinite-state processes. In TACAS'07. Google ScholarDigital Library
- P. Bouyer. A logical characterization of data languages. Inf. Processing Letters, 84(2), 2002. Google ScholarDigital Library
- P. Bouyer, A. Petit, and D. Thérien. Algebraic approach to data languages and timed languages. Inf. and Comp., 182(2), 2003. Google ScholarDigital Library
- M. Brambilla, S. Ceri, S. Comai, P. Fraternali, and I. Manolescu. Specification and design of workflow-driven hypertexts. Journal of Web Engineering, 1(1), 2002. Google ScholarDigital Library
- O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification of infinite structures. In Handbook of Process Algebra, pages 545--623. Elsevier Science, 2001.Google ScholarCross Ref
- D. Calvanese, G. De Giacomo, and M. Montali. Foundations of data-aware process analysis: a database theory perspective. In PODS, 2013. Google ScholarDigital Library
- S. Ceri, P. Fraternali, A. Bongio, M. Brambilla, S. Comai, and M. Matera. Designing data-intensive Web applications. Morgan-Kaufmann, 2002. Google ScholarDigital Library
- T. Chao et al. Artifact-based transformation of IBM Global Financing: A case study. In BPM, 2009. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.Google ScholarDigital Library
- D. Cohn, P. Dhoolia, F. Heath, F. Pinel, and J. Vergo. Siena: From powerpoint to web app in 5 minutes. In ICSOC, 2008. Google ScholarDigital Library
- E. Damaggio, A. Deutsch, and V. Vianu. Artifact systems with data dependencies and arithmetic. In ICDT, 2011. Google ScholarDigital Library
- E. Damaggio, R. Hull, and R. Vaculín. On the equivalence of incremental and fixpoint semantics for business artifacts with guard-stage-milestone lifecycles. Information Systems, 38:561--584, 2013. Google ScholarDigital Library
- G. De Giacomo, R. D. Masellis, and R. Rosati. Verification of conjunctive artifact-centric services. Int. J. Cooperative Inf. Syst., 21(2):111--140, 2012.Google ScholarCross Ref
- H. de Man. Case management: Cordys approach. BP Trends (www.bptrends.com), 2009.Google Scholar
- S. Demri and R. Lazić. LTL with the Freeze Quantifier and Register Automata. In LICS, 2006. Google ScholarDigital Library
- S. Demri, R. Lazić, and A. Sangnier. Model checking freeze LTL over one-counter automata. In FoSSaCS, 2008. Google ScholarDigital Library
- A. Deutsch, R. Hull, F. Patrizi, and V. Vianu. Automatic verification of data-centric business processes. In ICDT, 2009. Google ScholarDigital Library
- A. Deutsch, Y. Li, D. Lorant, and V. Vianu. Personal communication, 2014.Google Scholar
- A. Deutsch, M. Marcus, L. Sui, V. Vianu, and D. Zhou. A verifier for interactive, data-driven web applications. In SIGMOD, 2005. Google ScholarDigital Library
- A. Deutsch, L. Sui, and V. Vianu. Specification and verification of data-driven web services. In PODS, 2004. Google ScholarDigital Library
- A. Deutsch, L. Sui, and V. Vianu. Specification and verification of data-driven web applications. JCSS, 73(3):442--474, 2007. Google ScholarDigital Library
- A. Deutsch, L. Sui, and V. Vianu. Specification and verification of data-driven web services. JCSS, 73(3):442--474, 2007. Google ScholarDigital Library
- A. Deutsch, L. Sui, V. Vianu, and D. Zhou. A system for specification and verification of interactive, data-driven Web applications. In SIGMOD, 2006. Google ScholarDigital Library
- A. Deutsch, L. Sui, V. Vianu, and D. Zhou. Verification of communicating data-driven Web services. In PODS, pages 90--99, 2006. Google ScholarDigital Library
- G. Dong, R. Hull, B. Kumar, J. Su, and G. Zhou. A framework for optimizing distributed workflow executions. In DBPL, 1999. Google ScholarDigital Library
- E. A. Emerson. Temporal and modal logic. In J. V. Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pages 995--1072. North-Holland Pub. Co. MIT Press, 1990. Google ScholarDigital Library
- R. Fagin, P. G. Kolaitis, R. J. Miller, and L. Popa. Data exchange: Semantics and query answering. In ICDT, 2003. Google ScholarDigital Library
- M. F. Fernández, D. Florescu, A. Y. Levy, and D. Suciu. Declarative specification of web sites with Strudel. VLDB Journal, 9(1), 2000. Google ScholarDigital Library
- D. Florescu, K. Yagoub, P. Valduriez, and V. Issarny. WEAVE: A data-intensive web site management system(software demonstration). In EDBT, 2000.Google Scholar
- C. E. Gerede, K. Bhattacharya, and J. Su. Static analysis of business artifact-centric operational models. In SOCA, 2007. Google ScholarDigital Library
- C. E. Gerede and J. Su. Specification and verification of artifact behaviors in business process models. In ICSOC, 2007. Google ScholarDigital Library
- R. Glushko and T. McGrath. Document Engineering: Analyzing and Designing Documents for Business Informatics and Web Services. MIT Press, Cmabridge, MA, 2005. Google ScholarDigital Library
- B. B. Hariri, D. Calvanese, G. De Giacomo, A. Deutsch, and M. Montali. Verification of relational data-centric dynamic systems with external services. In PODS, 2013. Google ScholarDigital Library
- R. Hull, E. Damaggio, R. D. Masellis, F. Fournier, M. Gupta, F. H. III, S. Hobson, M. Linehan, S. Maradugu, A. Nigam, P. Sukaviriya, and R. Vaculín. Business artifacts with guard-stage-milestone lifecycles: Managing artifact interactions with conditions and events. In ACM DEBS, 2011. Google ScholarDigital Library
- R. Hull, F. Llirbat, B. Kumar, G. Zhou, G. Dong, and J. Su. Optimization techniques for data-intensive decision flows. In ICDE, 2000.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- R. Hull and J. Su. Tools for design of composite web services. In SIGMOD, 2004. Google ScholarDigital Library
- R. Hull, J. Su, and R. Vaculín. Data management perspectives on business process management: tutorial overview. In SIGMOD, 2013. Google ScholarDigital Library
- M. Jurdzinski and R. Lazić. Alternation-free modal mu-calculus for data trees. In LICS, 2007. Google ScholarDigital Library
- S. Kumaran, P. Nandi, T. Heath, K. Bhaskaran, and R. Das. ADoc-oriented programming. In Symp. on Applications and the Internet (SAINT), 2003. Google ScholarDigital Library
- R. Lazić, T. Newcomb, J. Ouaknine, A. Roscoe, and J. Worrell. Nets with tokens which carry data. In ICATPN'07. Google ScholarDigital Library
- L. Libkin. Elements of Finite Model Theory. Springer, 2004. Google ScholarDigital Library
- R. Liu, K. Bhattacharya, and F. Y. Wu. Modeling business contexture and behavior using business artifacts. In CAiSE, 2007. Google ScholarDigital Library
- M. Marin, R. Hull, and R. Vaculín. Data centric bpm and the emerging case management standard: A short survey. In BPM Workshops, 2012.Google Scholar
- D. Martin et al. OWL-S: Semantic markup for web services, W3C Member Submission, November 2003. http://www.daml.org/services/.Google Scholar
- S. A. McIlraith, T. C. Son, and H. Zeng. Semantic web services. IEEE Intelligent Systems, 16(2):46--53, 2001. Google ScholarDigital Library
- G. Mecca, P. Merialdo, and P. Atzeni. Araneus in the era of XML. IEEE Data Engineering Bulletin, 22(3):19--26, 1999.Google Scholar
- S. Merz. Model checking: a tutorial overview. In Modeling and verification of parallel processes. Springer-Verlag New York, 2001. Google ScholarDigital Library
- M. L. Minsky. Computation: finite and infinite machines. Prentice-Hall, 1967. Google ScholarDigital Library
- P. Nandi and S. Kumaran. Adaptive business objects -- a new component model for business integration. In Proc. Intl. Conf. on Enterprise Information Systems, 2005.Google Scholar
- 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. Google ScholarDigital Library
- A. Nigam and N. S. Caswell. Business artifacts: An approach to operational specification. IBM Systems Journal, 42(3), 2003. Google ScholarDigital Library
- A. Pnueli. The temporal logic of programs. In FOCS, 1977. Google ScholarDigital Library
- L. Segoufin and S. Torunczyk. Automata based verification over linearly ordered data domains. In STACS, 2011.Google Scholar
- A. Sistla and E. Clarke. The complexity of propositional linear temporal logic. J. of the ACM, 32:733--749, 1985. Google ScholarDigital Library
- D. Solomakhin, M. Montali, S. Tessaris, and R. D. Masellis. Verification of artifact-centric systems: Decidability and modeling issues. In ICSOC, 2013.Google ScholarDigital Library
- M. Spielmann. Verification of relational transducers for electronic commerce. JCSS., 66(1):40--65, 2003. Google ScholarDigital Library
- W. M. P. van der Aalst. Process Mining. Springer, 2011.Google Scholar
- J. Wang and A. Kumar. A framework for document-driven workflow systems. In BPM, 2005. Google ScholarDigital Library
- W.-D. Zhu et al. Advanced Case Management with IBM Case Manager. Available at http://www.redbooks.ibm.com/abstracts/sg247929.html?Open.Google Scholar
Index Terms
Automatic Verification of Database-Centric Systems
Recommendations
Automatic verification of database transaction safety
Maintaining the integrity of databases is one of the promises of database management systems. This includes assuring that integrity constraints are invariants of database transactions. This is very difficult to accomplish efficiently in the presence of ...
Automatic verification of database-driven systems: a new frontier
ICDT '09: Proceedings of the 12th International Conference on Database TheoryWe describe a novel approach to verification of software systems centered around an underlying database. Instead of applying general-purpose techniques with only partial guarantees of success, it identifies restricted but reasonably expressive classes ...
Comments