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.
This work is sponsored by the CALCULEMUS! IHP-RTN EC project, contract code HPRN-CT-2000-00102, and has thus benefited of the financial contribution of the Commission through the IHP programme.
Chapter PDF
Similar content being viewed by others
Keywords
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
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.
R. Alur. Timed Automata. In Proc. CAV’99, pages 8–22, 1999.
A. Biere, A. Cimatti, E. M. Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. In Proc. TACAS’99, pages 193–207, 1999.
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.
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.
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.
M. Davis, G. Longemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7), 1962.
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.
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.
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.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.
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.
L. Lamport. A Fast Mutual-exclusion Algorithm. ACM Transactions on Computer Systems, 5(1), 1987.
K. G. Larsen, P. Pettersson, and W. Yi. Model-Checking for Real-Time Systems. In Fundamentals of Computation Theory, pages 62–88, 1995.
K.G. Larsen, C. Weise, W. Yi, and J. Pearson. Clock difference diagrams. Technical Report 98/99, DoCS, Uppsala University, Sweden, 1998.
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.
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.
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.
R. Sebastiani. Integrating SAT Solvers with Math Reasoners: Foundations and Basic Algorithms. Technical Report 0111-22, ITC-IRST, November 2001.
Ofer Shtrichmann. Tuning SAT Checkers for Bounded Model Checking. In Proc. CAV’2000, volume 1855 of LNCS. Springer, 2000.
Maria Sorea. Bounded model checking for timed automata. ENTCS, 68(5), 2002.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R. (2002). Bounded Model Checking for Timed Systems. In: Peled, D.A., Vardi, M.Y. (eds) Formal Techniques for Networked and Distributed Sytems — FORTE 2002. FORTE 2002. Lecture Notes in Computer Science, vol 2529. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36135-9_16
Download citation
DOI: https://doi.org/10.1007/3-540-36135-9_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00141-6
Online ISBN: 978-3-540-36135-0
eBook Packages: Springer Book Archive