SpringerLink
Log in

Formal Verification of Database Applications Using Predicate Abstraction

  • Original Research
  • Published:
SN Computer Science Aims and scope Submit manuscript

Abstract

Formal verification has gained paramount attention from both academia and industry over more than 4 decades. Intensive research in this direction has resulted in many verification approaches, covering almost all mainstream languages. Unfortunately, the research community has paid little attention to the verification problem of database applications, which demands different treatments due to the presence of external database states. To fill this research gap, in this paper, we propose model checking-based verification of database programs using Predicate Abstractions instrumented with Counterexample-Guided Abstraction Refinement (CEGAR). As compared to the literature, the proposed approach shows its competence to support crucial SQL features (aggregate functions, nested queries, NULL values, and set operations) and the embedding of SQL codes within the host-imperative language. The developed prototype tool DBcheck based on our theoretical foundation allows us to automatically verify PL/SQL codes and present a detailed analysis of the experimental results under various circumstances. For the chosen set of benchmark PL/SQL codes and relevant database properties, our experiment shows that only 38% of procedures are correct. In contrast, 62% of procedures violate the database properties. The primary cause of the latter case is mostly due to the acceptance of runtime inputs in SQL statements without proper checking. To the best of our knowledge, this is the first attempt to extend predicate abstraction-based verification to the case of database applications.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Germany)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17

Similar content being viewed by others

References

  1. Elmasri R, Navathe SB. Database systems, vol. 9. Boston, MA: Pearson Education; 2011.

    MATH  Google Scholar 

  2. Clarke EM, Grumberg O, Long DE. Model checking and abstraction. TOPLAS. 1994;16(5):1512–42. https://doi.org/10.1145/186025.186051.

    Article  Google Scholar 

  3. Jhala R, Majumdar R. Software model checking. ACM Comput Surv. 2009;41(4):1–54. https://doi.org/10.1145/1592434.1592438.

    Article  Google Scholar 

  4. Ball T, Levin V, Rajamani SK. A decade of software model checking with slam. Commun ACM. 2011;54(7):68–76. https://doi.org/10.1145/1965724.1965743.

    Article  Google Scholar 

  5. Ball T, Majumdar R, Millstein T, Rajamani SK. Automatic predicate abstraction of c programs. ACM SIGPLAN Notices. 2001;36(5):203–13. https://doi.org/10.1145/381694.378846.

    Article  Google Scholar 

  6. Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement. Conf CAV. 2000;. https://doi.org/10.1007/978-3-642-22110-1_45.

    Article  MATH  Google Scholar 

  7. Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker blast. STTT. 2007;9(5–6):505–25. https://doi.org/10.1007/s10009-007-0044-z.

    Article  Google Scholar 

  8. Clarke E, Kroening D, Sharygina N, Yorav K. Satabs: Sat-based predicate abstraction for ansi-c. TACAS. 2005;. https://doi.org/10.1007/978-3-540-31980-1_40.

    Article  MATH  Google Scholar 

  9. Kroening D, Weissenbacher G. Interpolation-based software verification with wolverine. Conf CAV. 2011;. https://doi.org/10.1007/978-3-642-22110-1_45.

    Article  Google Scholar 

  10. Bérard B, Bidoit M, Finkel A, Laroussinie F, Petit A, Petrucci L, Schnoebelen P. Systems and software verification: model-checking techniques and tools. New York: Springer; 2013.

    MATH  Google Scholar 

  11. Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B, Frama-c. in International Conference on Software Engineering and Formal Methods. Springer, 2012;233–247.

  12. Hoare CAR. An axiomatic basis for computer programming. Commun ACM. 1969;12(10):576–80.

    Article  Google Scholar 

  13. Itzhaky S, Kotek T, Rinetzky N, Sagiv M, Tamir O, Veith H, Zuleger F. On the automated verification of web applications with embedded sql. In Proc. of ICDT, 2017.

  14. Benzaken V, Schaefer X. Static management of integrity in object-oriented databases: Design and implementation. In: International Conference on Extending Database Technology. Springer, 1998;309–325.

  15. Christiansen H, Martinenghi D. Simplification of database integrity constraints revisited: A transformational approach. In: Int. Symposium on Logic-Based Program Synthesis and Transformation. Springer, 2003;178–197.

  16. Malecha G, Morrisett G, Shinnar A, Wisnesky R. Toward a verified relational database management system. ACM Sigplan Notices. 2010;45(1):237–48.

    Article  Google Scholar 

  17. Baltopoulos IG, Borgström J, Gordon AD. Maintaining database integrity with refinement types. In: European Conference on Object-Oriented Programming. Berlin, Heidelberg: Springer, 2011;484–509.

  18. Sharygina N, Kröning D. Model checking with abstraction for web services. In Test and Analysis of Web Services. Springer, 2007;121–145. https://doi.org/10.1007/978-3-540-72912-9_5.

  19. Deutsch A, Hull R, Vianu V. Automatic verification of database-centric systems. ACM SIGMOD Record. 2014;43(3):5–17. https://doi.org/10.1145/2694428.2694430.

    Article  Google Scholar 

  20. Deutsch A, Marcus M, Sui L, Vianu V, Zhou D. A verifier for interactive, data-driven web applications. In: Proceedings of the 2005 ACM SIGMOD int. conf. on Management of data. 2005. https://doi.org/10.1145/1066157.1066219.

  21. Diana R, Marques-Neto H, Zarate L, Song M. A symbolic model checking approach to verifying transact-sql. In In. Conf. on SMC. IEEE, 2012;1735–1741. https://doi.org/10.1109/icsmc.2012.6377988.

  22. Gligoric M, Majumdar R. Model checking database applications. In: Proceedings of TACAS. Springer, 2013;549–564. https://doi.org/10.1007/978-3-642-36742-7_40.

  23. Ullman JD. Database constraints. http://infolab.stanford.edu/~ullman/fcdb/jw-notes06/constraints.html. Accessed 20 Aug 2020.

  24. Project P. Github pl/sql project. https://github.com/topics/plsql. Accessed 29 July 2020.

  25. Jana A, Alam MI, Halder R, A symbolic model checker for database programs. In: ICSOFT, 2018;381–388. https://doi.org/10.5220/0006913003810388.

  26. Parr T, The definitive ANTLR 4 reference. Pragmatic Bookshelf, 2013.

  27. De Moura L, Bjørner N. “Z3: An efficient smt solver,” in Int. conf. on TACAS. Springer, 2008;337–340.

  28. Halder R, Cortesi A. Abstract interpretation of database query languages. Comput Lang Syst Struct. 2012;38(2):123–57. https://doi.org/10.1016/j.cl.2011.10.004.

    Article  MATH  Google Scholar 

  29. Jana A, Halder R, Kalahasti A, Ganni S, Cortesi A. Extending abstract interpretation to dependency analysis of database applications. TSE. 2018;46(5):463–94. https://doi.org/10.1109/tse.2018.2861707.

    Article  Google Scholar 

  30. Ball T, Rajamani SK, Bebop: A symbolic model checker for boolean programs. In Int. SPIN Workshop on Model Checking of Software. Berlin, Heidelberg: Springer, 2000;113–130. https://doi.org/10.1007/10722468_7.

  31. Aycock J, Horspool N, Simple generation of static single-assignment form. In Compiler Construction, D. A. Watt, Ed. Berlin, Germany: Springer, Berlin Heidelberg, March 25–April 2 2000;110–125, https://doi.org/10.1007/3-540-46423-9_8.

  32. Weiser M. Program slicing. TSE. 1984;4:352–7. https://doi.org/10.1109/tse.1984.5010248.

    Article  MATH  Google Scholar 

  33. Ball T, Rajamani SK. “Generating abstract explanations of spurious counterexamples in c programs,” Technical Report MSR-TR-2002-09, Microsoft Research, Tech. Rep., (2002).

  34. Winskel G. The formal semantics of programming languages: an introduction. New York: MIT Press; 1993.

    Book  Google Scholar 

  35. Furia CA, Meyer B, Velder S. Loop invariants: analysis, classification, and examples. ACM Comput Surv (CSUR). 2014;46(3):34.

    Article  Google Scholar 

  36. Kroening D, Weissenbacher G. Verification and falsification of programs with loops using predicate abstraction. Formal Aspects Comput. 2010;22(2):105–128.

    Article  Google Scholar 

  37. Cortesi A, Halder R. Abstract interpretation of recursive queries. In International Conference on Distributed Computing and Internet Technology. Springer, 2013;157–170.

  38. Briggs P, Cooper KD, Harvey TJ, Simpson LT. Practical improvements to the construction and destruction of static single assignment form. SP&E. 1998;28(8):859–81. https://doi.org/10.1002/(sici)1097-024x(19980710)28:8<859::aid-spe188>3.0.co;2-8.

    Article  Google Scholar 

  39. Beyer D. Software verification with validation of results. In TACAS. Springer, 2017;331–349.

Download references

Funding

This research was funded by IMPRINT-2 Project (IMP/2018/000523) from the Science and Engineering Research Board (SERB), Department of Science and Technology, Government of India.

Author information

Authors and Affiliations

  1. Indian Institute of Technology Patna, Patna, India

    Md Imran Alam & Raju Halder

  2. Università Ca’ Foscari Venezia, Venezia, Italy

    Md Imran Alam

Authors
  1. Md Imran Alam
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Raju Halder
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Md Imran Alam.

Ethics declarations

Conflict of interest

On behalf of all authors, the corresponding author states that there is no conflict of interest.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This article is part of the topical collection “Applications of Software Engineering and Tool Support” guest edited by Nabendu Chaki, Agostino Cortesi and Anirban Sarkar.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Alam, M.I., Halder, R. Formal Verification of Database Applications Using Predicate Abstraction. SN COMPUT. SCI. 2, 135 (2021). https://doi.org/10.1007/s42979-020-00426-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s42979-020-00426-2

Keywords

Search

Navigation