Verifying Parameterized taDOM+ Lock Managers | SpringerLink
Skip to main content
Springer Nature Link
Log in

Verifying Parameterized taDOM+ Lock Managers

  • Conference paper
SOFSEM 2008: Theory and Practice of Computer Science (SOFSEM 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4910))

Abstract

taDOM* protocols are designed to provide lock-based approach to handle multiple access to XML databases. The notion of taDOM+ protocol is formalized and generalized and a formal model of taDOM+ lock manager that is parameterized in the number of transactions and in the size of database is represented. An important class of safety properties of taDOM+ lock managers were proven to be checked by examining just a small number of finite-state instances of the parameterized model. Our results were applied to prove a generalized mutual exclusion property, known as repeatable-read, of taDOM2+ and taDOM3+ lock managers by model-checking.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Alpern, B., Schneider, F.B.: Defining Liveness. Inf. Process. Lett. 21, 181–185 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  2. Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inform. Process. Lett. 22, 307–309 (1986)

    Article  MathSciNet  Google Scholar 

  3. Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems with many similar processes. ACM T. Progr. Lang. Sys., 51–115 (1998)

    Google Scholar 

  4. Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Method. Syst. Des. 9, 77–104 (1996)

    Article  Google Scholar 

  5. Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms. MIT Press, Cambridge (2001)

    MATH  Google Scholar 

  6. Creese, S.J.: Data Independent Induction: CSP Model Checking of Arbitrary Sized Networks. Ph.D. thesis, Oxford University (2001)

    Google Scholar 

  7. Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol. 1831, pp. 236–254. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  8. Emerson, E. A., Kahlon, V.: Model checking guarded protocols. In: Proc. LICS 2003, Ottawa, pp. 361–370 (2003)

    Google Scholar 

  9. Emerson, E.A., Kahlon, V.: Exact and efficient verification of parameterized cache coherence protocols. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 247–262. Springer, Heidelberg (2003)

    Google Scholar 

  10. Emerson, E.A., Kahlon, V.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 325–339. Springer, Heidelberg (2004)

    Google Scholar 

  11. Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: Proc. POPL 1995, San Francisco, pp. 85–94 (1995)

    Google Scholar 

  12. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Method. Syst. Des. 9, 105–131 (1996)

    Article  Google Scholar 

  13. German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39, 675–735 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  14. Haustein, M., Härder, T.: Optimizing concurrent XML processing. Internal report, Kaiserslautern University of Technology (2005), http://wwwlgis.informatik.uni-kl.de/archiv/wwwdvs.informatik.uni-kl.de/pubs/papers/HH05.Int-Report.pdf

  15. Haustein, M., Härder, T.: An efficient infrastructure for native transactional XML processing. Data Knowl. Eng. 61, 500–523 (2007)

    Article  Google Scholar 

  16. Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Verifying sequential consistency on shared-memory multiprocessor systems. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 301–315. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Ip, N., Dill, D.: Better verification through symmetry. Form. Method. Syst. Des. 9, 41–75 (1996)

    Article  Google Scholar 

  18. Ip, N., Dill, D.: Verifying systems with replicated components in Murϕ. Form. Method. Syst. Des. 14, 273–310 (1999)

    Article  Google Scholar 

  19. Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. Inf. Comp. 117, 1–11 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  20. Lazić, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. Ph.D. thesis. Oxford University (2001)

    Google Scholar 

  21. Li, J., Suzuki, I., Yamashita, M.: A new structural induction theorem for rings of temporal Petri nets. IEEE T. Software Eng. 20, 115–126 (1994)

    Article  Google Scholar 

  22. Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized networks of processes. Theor. Comput. Sci. 256, 113–144 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  23. Lubachevsky, B.D.: An approach to automating the verifcation of compact parallel coordination programs I. Acta Inform. 21, 125–169 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  24. Pyssysalo, T.: An Induction Theorem for Ring Protocols of Processes Described with Predicate/Transition Nets. Research Reports, Helsinki University of Technology A37 (1996)

    Google Scholar 

  25. Ramakrishnan, R., Gehrke, J.: Database Management Systems, 3rd edn. McGraw Hill, New York (2002)

    Google Scholar 

  26. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1997)

    Google Scholar 

  27. World Wide Web Consortium, http://www.w3c.org/

  28. Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1990)

    Google Scholar 

  29. Appendix, http://www.tol.oulu.fi/~santti/papers/tadom_appendix.pdf

Download references

Author information

Authors and Affiliations

  1. Department of Information Processing Science, University of Oulu, PL 3000, 90014 University of Oulu, Finland

    Antti Siirtola

  2. Faculty of Electrical Engineering, Department of Computer Science and Engineering, Czech Technical University in Prague, Karlovo námesti 13, 121 35, Prague 2, Czech Republic

    Michal Valenta

Authors
  1. Antti Siirtola
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michal Valenta
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Viliam Geffert Juhani Karhumäki Alberto Bertoni Bart Preneel Pavol Návrat Mária Bieliková

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Siirtola, A., Valenta, M. (2008). Verifying Parameterized taDOM+ Lock Managers. In: Geffert, V., Karhumäki, J., Bertoni, A., Preneel, B., Návrat, P., Bieliková, M. (eds) SOFSEM 2008: Theory and Practice of Computer Science. SOFSEM 2008. Lecture Notes in Computer Science, vol 4910. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77566-9_40

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-77566-9_40

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-77565-2

  • Online ISBN: 978-3-540-77566-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation