Skip to main content
SpringerLink
Log in

Efficient Real-Time Model Checking Using Tabled Logic Programming and Constraints

  • Conference paper
  • First Online:
Logic Programming (ICLP 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2401))

Included in the following conference series:

Abstract

Logic programming based tools for real-time model checking are beginning to emerge. In a previous work we had demonstrated the feasibility of building such a model checker by combining constraint processing and tabulation. But efficiency and practicality of such a model checker were not adequately addressed. In this paper we describe XMC/dbm, an efficient model checker for real-time systems using tabling. Performance gains in XMC/dbmdirectly arise from the use of a lightweight constraint solver combined with tabling. Specifically the timing constraints are represented by difference bound matrices which are encoded as Prolog terms. Operations on these matrices, the dominant component in real-time model checking, are shared using tabling. We provide experimental evidence that the performance of XMC/dbmis considerably better than our previous real-time model checker and is highly competitive to other well known real-time model checkers implemented in C/C++. An important aspect of XMC/dbm is that it can handle verification of systems consisting of untimed components with performance comparable to verification systems built specifically for untimed systems.

This work was supported in part by NSF grants EIA-9705998, CCR-9876242, and IIS-0072927.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  2. S. Basu, S. A. Smolka, and O. R. Ward. Model checking the Java Meta-Locking algorithm. In Proceedings of 7th IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2000), Edinburgh, Scotland, April 2000.

    Google Scholar 

  3. J. Bengtsson, W. O. D. Griffioen, K. J. Kristoffersen, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi. Verification of an audio protocol with bus collision using Uppaal. In Proceedings of the 8th International Conference on Computer-Aided Verification, volume 1102 of LNCS, pages 244–256, New Brunswick, New Jersey, USA, 1996. Springer-Verlag.

    Google Scholar 

  4. T. H. Cormen, C. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, 1999.

    Google Scholar 

  5. G. Delzanno and S. Etalle. Transforming a proof system into prolog for verifying security protocols. In International Workshop on Logic-based Program Synthesis and Transformation, November 2001.

    Google Scholar 

  6. G. Delzanno, S. Mukhopadhyay, and A. Podelski. Constraint-based model checking for timed systems with accurate widenings. Technical Report, Max-Planck-Institut für Informatik, 1999.

    Google Scholar 

  7. G. Delzanno and A. Podelski. Model checking in CLP. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’ 99), LNCS, volume 1579, pages 223–239, Amsterdam, March 1999.

    Chapter  Google Scholar 

  8. D. L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Proceedings of CAV’89. LNCS 407, 1989.

    Google Scholar 

  9. X. Du, C. R. Ramakrishnan, and S. A. Smolka. Tabled resolution + constraints: a recipe for model checking real-time systems. In Proceedings of the IEEE Real-Time Systems Symposium. IEEE Computer Society Press, 2000.

    Google Scholar 

  10. F. Fioravanti, A. Pettorossi, and M. Proietti. Verification of sets of infinite state processes using program transofmration. In International Workshop on Logic-based Program Synthesis and Transformation, November 2001.

    Google Scholar 

  11. G. Gupta and E. Pontelli. A Constraint Based Approach for Specification and Verification of Real-Time Systems. In Proceedings of the IEEE Real-Time Systems Symposium, December 1997.

    Google Scholar 

  12. N. Halbwachs, Y. E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, August 1997.

    Google Scholar 

  13. T. A. Henzinger, P. H. Ho, and H. Wong-Toi. “HyTech: A model checker for hybrid systems”. International Journal on Software Tools for Technology Transfer, 1(2):110–122, October 1997.

    Google Scholar 

  14. G. J. Holzmann. The model checker SPIN. IEEE Transactions on Software Engineering, 23(5):279–295, May 1997.

    Google Scholar 

  15. K. G. Larsen, P. Pettersson, and W. Yi. Model checking for real-time systems. In Proc. of Fundamentals of Computation Theory, number 965 in LNCS, pages 62–88, August 1995.

    Google Scholar 

  16. K. G. Larsen, P. Pettersson, and W. Yi. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer, 1:134–152, 1997.

    Article  MATH  Google Scholar 

  17. M. Leuschel and S. Gruner. Abstract partial deduction using regular types and its application to model checking. In International Workshop on Logic-based Program Synthesis and Transformation, November 2001.

    Google Scholar 

  18. U. Nilsson and J. Lubcke. Constraint logic programming for local and symbolic model-checking. In In Proc. of the Int’l Conf. on Computational Logic (CL2000), volume 1861. Springer-Verlag, 2000.

    Google Scholar 

  19. Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In Proceedings of the 9th International Conference on Computer-Aided Verification (CAV’ 97), volume 1254 of LNCS, pages 143–154, Haifa, Israel, July 1997. Springer-Verlag.

    Google Scholar 

  20. C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, Y. Dong, X. Du, A. Roychoudhury, and V. N. Venkatakrishnan. XMC: A logic-programming-based verification toolset. In Proceedings of the 12th International Conference on Computer-Aided Verification (CAV’ 00), pages 576–580. Springer-Verlag, 2000.

    Google Scholar 

  21. A. Roychoudhury and I. V. Ramakrishnan. Automated inductive verification of parameterized protocols. In Proceedings of the 13th International Conference on Computer-Aided Verification (CAV’ 01), volume 2102 of LNCS. Springer-Verlag, 2001.

    Google Scholar 

  22. O. Sokolsky and S. A. Smolka. Local model checking for real-time systems. In Proceedings of the 7th International Conference on Computer-Aided Verification, volume 939 of LNCS. American Mathematical Society, 1995.

    Google Scholar 

  23. L. Urbina. Analysis of hybrid systems in CLP(R). In Constraint Programming (CP’96), volume LNCS 1102. Springer-Verlag, 1996.

    Google Scholar 

  24. XSB. The XSB logic programming system. Available at www.cs.sunysb.edu/~sbprolog .

  25. S. Yovine. Model checking timed automata. In European Educational Forum: School on Embedded Systems, pages 114–152, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, State University of New York at Stony Brook, Stony Brook, New York, USA

    Giridhar Pemmasani, C. R. Ramakrishnan & I. V. Ramakrishnan

Authors
  1. Giridhar Pemmasani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. C. R. Ramakrishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. I. V. Ramakrishnan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Software Engineering, University of Melbourne, 221 Bouverie St., Carlton, 3053, Australia

    Peter J. Stuckey

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pemmasani, G., Ramakrishnan, C.R., Ramakrishnan, I.V. (2002). Efficient Real-Time Model Checking Using Tabled Logic Programming and Constraints. In: Stuckey, P.J. (eds) Logic Programming. ICLP 2002. Lecture Notes in Computer Science, vol 2401. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45619-8_8

Download citation

  • DOI: https://doi.org/10.1007/3-540-45619-8_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43930-1

  • Online ISBN: 978-3-540-45619-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation