Automatic verification of database-driven systems: a new frontier

ABSTRACT

We 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 of applications and properties for which sound and complete verification can be performed in a fully automatic way. This leverages the emergence of high-level specification tools for database-centered applications that not only allow fast prototyping and improved programmer productivity but, as a side effect, provide convenient targets for automatic verification. We present theoretical and practical results on verification of database-driven systems. The results are quite encouraging and suggest that, unlike arbitrary software systems, significant classes of database-driven systems may be amenable to automatic verification. This relies on a novel marriage of database and model checking techniques, of relevance to both the database and the computer aided verification communities.

REFERENCES

• 1: Martín Abadi , Leslie Lamport , Pierre Wolper, Realizable and Unrealizable Specifications of Reactive Systems, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, p.1-17, July 11-15, 1989
• 2: Serge Abiteboul , Omar Benjelloun , Tova Milo, The Active XML project: an overview, The VLDB Journal — The International Journal on Very Large Data Bases, v.17 n.5, p.1019-1040, August 2008 [doi>10.1007/s00778-007-0049-y]
• 3: 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]
• 4: Serge Abiteboul , Richard Hull , Victor Vianu, Foundations of Databases: The Logical Level, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 5: 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]
• 6: 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]
• 7: Nabil R. Adam , Vijayalakshmi Atluri , Wei-Kuang Huang, Modeling and Analysis of Workflows Using Petri Nets, Journal of Intelligent Information Systems, v.10 n.2, p.131-158, March/April 1998 [doi>10.1023/A:1008656726700]
• 8: Daniela Berardi , Diego Calvanese , Giuseppe De Giacomo , Richard Hull , Massimo Mecella, Automatic composition of transition-based semantic web services with messaging, Proceedings of the 31st international conference on Very large data bases, August 30-September 02, 2005, Trondheim, Norway
• 9: D. Berardi, D. Calvanese, G. D. Giacomo, R. Hull, M. Lenzerini, and M. Mecella. Modeling data & processes for service specifications in Colombo. In EMOI-INTEROP, 2005.
• 10: D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. Automatic composition of e-services that export their behavior. In Proc. Int'l. Conf on Service-Oriented Computing (ICSOC), pages 43--58, 2003.
• 11: D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. E-service composition by description logics based reasoning. In Description Logics, 2003.
• 12: D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. A tool for automatic composition of services based on logics of programs. In Technologies for E-Services, 5th International Workshop (TES), pages 80--94, 2004.
• 13: D. Berardi, D. Calvanese, G. D. Giacomo, M. Lenzerini, and M. Mecella. Automatic service composition based on behavioral descriptions. Int. J. Cooperative Inf. Syst., 14(4):333--376, 2005.
• 14: Daniela Berardi , Giuseppe De Giacomo , Maurizio Lenzerini , Massimo Mecella , Diego Calvanese, Synthesis of underspecified composite e-services based on automated reasoning, Proceedings of the 2nd international conference on Service oriented computing, November 15-19, 2004, New York, NY, USA [doi>10.1145/1035167.1035183]
• 15: 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]
• 16: Anthony J. Bonner , Michael Kifer, An overview of transaction logic, Theoretical Computer Science, v.133 n.2, p.205-265, Oct. 24, 1994 [doi>10.1016/0304-3975(94)90190-2]
• 17: 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]
• 18: 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]
• 19: 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.
• 20: 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]
• 21: 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]
• 22: BPML.org. Business process modeling language. http://www.bpmi.org.
• 23: 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.
• 24: Daniel Brand , Pitro Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM (JACM), v.30 n.2, p.323-342, April 1983 [doi>10.1145/322374.322380]
• 25: Tevfik Bultan , Xiang Fu , Richard Hull , Jianwen Su, Conversation specification: a new approach to design and analysis of e-service composition, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary [doi>10.1145/775152.775210]
• 26: O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification of infinite structures. In Handbook of Process Algebra, pages 545--623. Elsevier Science, 2001.
• 27: Stefano Ceri , Piero Fraternali , Aldo Bongio , Marco Brambilla , Sara Comai , Maristella Matera, Designing Data-Intensive Web Applications, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2002
• 28: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
• 29: C. Courcoubetis , M. Vardi , P. Wolper , M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, v.1 n.2-3, p.275-288, Oct. 1992 [doi>10.1007/BF00121128]
• 30: Mark H. Burstein , Jerry R. Hobbs , Ora Lassila , David Martin , Drew V. McDermott , Sheila A. McIlraith , Srini Narayanan , Massimo Paolucci , Terry R. Payne , Katia P. Sycara, DAML-S: Web Service Description for the Semantic Web, Proceedings of the First International Semantic Web Conference on The Semantic Web, p.348-363, June 09-12, 2002
• 31: Hasan Davulcu , Michael Kifer , C. R. Ramakrishnan , I. V. Ramakrishnan, Logic based modeling and analysis of workflows, Proceedings of the seventeenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.25-33, June 01-04, 1998, Seattle, Washington, United States [doi>10.1145/275487.275491]
• 32: 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]
• 33: S. Demri, R. Lazić, and A. Sangnier. Model checking freeze LTL over one-counter automata. In Proc. 11th Int'l. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS'08), pages 490--504, 2008.
• 34: Alin Deutsch , Richard Hull , Fabio Patrizi , Victor Vianu, Automatic verification of data-centric business processes, Proceedings of the 12th International Conference on Database Theory, March 23-25, 2009, St. Petersburg, Russia [doi>10.1145/1514894.1514924]
• 35: 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]
• 36: Alin Deutsch , Liying Sui , Victor Vianu, Specification and verification of data-driven web services, Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 14-16, 2004, Paris, France [doi>10.1145/1055558.1055571]
• 37: 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]
• 38: 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]
• 39: 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]
• 40: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 41: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 42: Mary Fernández , Daniela Florescu , Alon Levy , Dan Suciu, Declarative specification of Web sites with S, The VLDB Journal — The International Journal on Very Large Data Bases, v.9 n.1, p.38-55, March 2000 [doi>10.1007/s007780050082]
• 43: D. Florescu, K. Yagoub, P. Valduriez, and V. Issarny. WEAVE: A data-intensive web site management system(software demonstration). In Proc. of the Conf. on Extending Database Technology (EDBT), 2000.
• 44: J. Garson. Quantification in modal logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, pages 249--307. Reidel, 1977.
• 45: Dimitrios Georgakopoulos , Mark Hornick , Amit Sheth, An overview of workflow management: from process modeling to workflow automation infrastructure, Distributed and Parallel Databases, v.3 n.2, p.119-153, April 1995 [doi>10.1007/BF01277643]
• 46: D. Harel. On the formal semantics of statecharts. In Proc. IEEE Conf. on Logic in Computer Science (LICS), pages 54--64, 1987.
• 47: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 48: G. Hughes and M. Cresswell. An introduction to modal logic. Methuen, 1968.
• 49: Richard Hull , Michael Benedikt , Vassilis Christophides , Jianwen Su, E-services: a look behind the curtain, Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, p.1-14, June 09-11, 2003, San Diego, California [doi>10.1145/773153.773154]
• 50: Richard Hull , Jianwen Su, Tools for design of composite Web services, Proceedings of the 2004 ACM SIGMOD international conference on Management of data, June 13-18, 2004, Paris, France [doi>10.1145/1007568.1007722]
• 51: 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]
• 52: Orna Kupferman , Moshe Y. Vardi, Synthesizing Distributed Systems, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.389, June 16-19, 2001
• 53: 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.
• 54: G. Mecca, P. Merialdo, and P. Atzeni. Araneus in the era of XML. IEEE Data Engineering Bulletin, 22(3):19--26, 1999.
• 55: Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
• 56: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 57: W. Mok and D. Paper. Using harel's statecharts to model business workflows. J. of Database Management, 13(3):17--34, 2002.
• 58: 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]
• 59: A. Pneuli , R. Rosner, Distributed reactive systems are hard to synthesize, Proceedings of the 31st Annual Symposium on Foundations of Computer Science, p.746-757 vol.2, October 22-24, 1990 [doi>10.1109/FSCS.1990.89597]
• 60: E. L. Post. Recursive unsolvability of a problem of Thue. J. of Symbolic Logic, 12:1--11, 1947.
• 61: Knowlege in action: logical foundations for specifying and implementing dynamical systems, MIT Press, Cambridge, MA, 2001
• 62: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• 63: A. Prasad Sistla , M. Y. Vardi , P. Wolper, The complementation problem for Bu¨chi automata with applications to temporal logic, Theoretical Computer Science, v.49 n.2-3, p.217-237, January 1987 [doi>10.1016/0304-3975(87)90008-9]
• 64: 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]
• 65: B. Trankhtenbrot. The impossibility of an algorithm for the decision problem for finite models. Doklady Academii Nauk SSSR, 70:569--572, 1950.
• 66: W. M. P. van der Aalst. The application of petri nets to workflow management. Journal of Circuits, Systems, and Computers, 8(1):21--66, 1998.
• 67: W. M. P. van der Aalst and A. H. M. ter Hofstede. Workflow patterns: On the expressive power of (petri-net-based) workflow languages. In Proc. of the Fourth International Workshop on Practical Use of Coloured Petri Nets and the CPN Tools, Aarhus, Denmark, August 28--30, 2002 / Kurt Jensen (Ed.), pages 1--20. Technical Report DAIMI PB-560, Aug. 2002. InternalNote: Submitted by: hr available online: http://www.daimi.aau.dk/CPnets/workshop02/cpn/papers/.
• 68: M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. IEEE Conf. on Logic in Computer Science (LICS), pages 332--344, 1986.
• 69: Dirk Wodtke , Gerhard Weikum, A Formal Foundation for Distributed Workflow Execution Based on State Charts, Proceedings of the 6th International Conference on Database Theory, p.230-246, January 08-10, 1997
• 70: Workflow management coalition, 2001. http://www.wfmc.org.
• 71: Web Services Flow Language(WSFL 1.0), 2001. http://www-3.ibm.com/software/solutions/webservices/pdf/WSFL.pdf.