Advertisement

Bounded Model Checking for Timed Systems

  • G. Audemard
  • A. Cimatti
  • A. Kornilowicz
  • R. Sebastiani
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)

Abstract

Enormous progress has been achieved in the last decade in the verification of timed systems, making it possible to analyze significant real-world protocols. An open challenge is the identification of fully symbolic verification techniques, able to deal effectively with the finite state component as well as with the timing aspects. In this paper we propose a new, symbolic verification technique that extends the Bounded Model Checking (BMC) approach for the verification of timed systems. The approach is based on the following ingredients. First, a BMC problem for timed systems is reduced to the satisfiability of a math-formula, i.e., a boolean combination of propositional variables and linear mathematical relations over real variables (used to represent clocks). Then, an appropriate solver, called MathSAT, is used to check the satisfiability of the math-formula. The solver is based on the integration of SAT techniques with some specialized decision procedures for linear mathematical constraints, and requires polynomial memory. Our methods allow for handling expressive properties in a fully-symbolic way. A preliminary experimental evaluation confirms the potential of the approach.

Keywords

Model Check Mutual Exclusion Boolean Variable Linear Temporal Logic Propositional Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [ABC+02]
    G. Audemard, P. Bertoli, A. Cimatti, A. Korni lowicz, and R. Sebastiani. A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. In Proc. CADE’2002., 2002.Google Scholar
  2. [Alu99]
    R. Alur. Timed Automata. In Proc. CAV’99, pages 8–22, 1999.Google Scholar
  3. [BCCZ99]
    A. Biere, A. Cimatti, E. M. Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. In Proc. TACAS’99, pages 193–207, 1999.Google Scholar
  4. [BDM+98]
    M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A model-checking tool for real-time systems. In A. J. Hu and M. Y. Vardi, editors, Proc. 10th International Conference on Computer Aided Verification, Vancouver, Canada, volume 1427 of LNCS, pages 546–550. Springer-Verlag, 1998.Google Scholar
  5. [CFG+01]
    F. Copty, L. Fix, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Vardi. Benefits of Bounded Model Checking at an Industrial Setting. In Proc. CAV’2001, LNCS. Springer, 2001.Google Scholar
  6. [Dil89]
    David L. Dill. Timing assumptions and verification of finite-state concurrent systems. InAutomatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pages 197–212. Springer-Verlag, June 1989.Google Scholar
  7. [DLL62]
    M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.Google Scholar
  8. [DY95]
    C. Daws and S. Yovine. Two examples of verification of multirate timed automata with kronos. In Proc. 16th IEEE Real-Time Systems Symposium, pages 66–75, 1995.Google Scholar
  9. [Eme90]
    E.A. Emerson. Temporal and Modal Logic. InJ. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier Science Publisher B.V., 1990.Google Scholar
  10. [GMS98]
    E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability. In Proc. AAAI’98, pages 948–953, 1998.Google Scholar
  11. [HNSY94]
    T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  12. [LA97]
    Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pages 366–371, 1997.Google Scholar
  13. [Lam87]
    L. Lamport. A Fast Mutual-exclusion Algorithm. ACM Transactions on Computer Systems, 5(1), 1987.Google Scholar
  14. [LPY95]
    K. G. Larsen, P. Pettersson, and W. Yi. Model-Checking for Real-Time Systems. In Fundamentals of Computation Theory, pages 62–88, 1995.Google Scholar
  15. [LWYP98]
    K.G. Larsen, C. Weise, W. Yi, and J. Pearson. Clock difference diagrams. Technical Report 98/99, DoCS, Uppsala University, Sweden, 1998.Google Scholar
  16. [MLAH01]
    J. Moeller, J. Lichtenberg, H. Andersen, and H. Hulgaard. Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams. In Electronic Notes in Theoretical Computer Science, volume 23. Elsevier Science, 2001.Google Scholar
  17. [NMA+02]
    P. Niebert, M. Mahfoudh, E. Asarin, M. Bozga, and O. Maler. Verification of Timed Automata via Satisfiability Checking. In Proc. of FTRTFT’02, LNCS. Springer-Verlag, 2002.Google Scholar
  18. [PWZ02]
    W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of FTRTFT’02, LNCS. Springer-Verlag, 2002.Google Scholar
  19. [Seb01]
    R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001.Google Scholar
  20. [Sht00]
    Ofer Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV’2000, volume 1855 of LNCS. Springer, 2000.Google Scholar
  21. [Sor02]
    Maria Sorea. Bounded model checking for timed automata. ENTCS, 68(5), 2002.Google Scholar
  22. [Wan00]
    Farn Wang. Efficient data structure for fully symbolic verification of real-time software systems. InTools and Algorithms for Construction and Analysis of Systems, pages 157–171, 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • G. Audemard
    • 1
  • A. Cimatti
    • 1
  • A. Kornilowicz
    • 1
  • R. Sebastiani
    • 1
    • 2
  1. 1.ITC-IRSTPovoItaly
  2. 2.DIT, Università di TrentoPovoItaly

Personalised recommendations