Abstract
Based on the equivalence relation for location based reachability between continuous and integer semantics of closed timed automata, Beyer et al. have implemented the verifier Rabbit, with the uniform representation of reachable configurations. However, the growth of maximal constant of clock variables will decline the performance of Rabbit. The paper proposes an improved symbolic method, using binary decision diagrams (BDDs) to store the symbolic representation of discretized states, for the verification of timed systems. Compared with Rabbit, experiments demonstrate that besides the memory reduction, our implementation is also less sensitive to the size of clock domain.
Supported by 973 Program of China under Grant No. 2002cb312200; and the National Natural Science Foundation of China under Grant Nos. 60673051, 60421001.
Chapter PDF
Similar content being viewed by others
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Asarin, E., Maler, O., Pnueli, A.: On discretization of delays in timed automata and digital circuits. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 470–484. Springer, London (1998)
Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Computer Aided Verification, pp. 341–353 (1999)
Bellman, R.: Dynamic Programming. Princeton University Press, Princeton (1957)
Beyer, D.: Improvements in BDD-based reachability analysis of timed automata. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 318–343. Springer, Heidelberg (2001)
Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A tool for BDD-based verification of real-time systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 122–125. Springer, Heidelberg (2003)
Beyer, D., Noack, A.: Can decision diagrams overcome state space explosion in real-time verification? In: König, H., Heiner, M., Wolisz, A. (eds.) FORTE 2003. LNCS, vol. 2767, pp. 193–208. Springer, Heidelberg (2003)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
Asarin, E., Bozga, M., Kerbrat, A., Maler, O., Pnueli, A., Rasse, A.: Data structures for the verification of timed automata. In: Maler, O. (ed.) Hybrid and Real-Time Systems, Grenoble, France. LNCS, pp. 346–360. Springer Verlag, Heidelberg (1997)
Gollü, A., Puri, A., Varaiya, P.: Discetization of timed automata. In: Proceedings of the 33rd IEEE conferene on decision and control, pp. 957–958 (1994)
Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio/video protocol: An industrial case study using UPPAAL. In: Proc. of the 18th IEEE Real-Time Systems Symposium, pp. 2–13. IEEE Computer Society Press, Los Alamitos (1997)
Lamport, L.: A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1–11 (1987)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 1(1-2), 134–152 (1997)
Lindahl, M., Pettersson, P., Yi, W.: Formal design and analysis of a gear controller. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, pp. 281–297. Springer, Heidelberg (1998)
Møller, J., Lichtenberg, J., Andersen, H.R., Hulgaard, H.: Difference decision diagrams. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 111–125. Springer, Heidelberg (1999)
Wang, F.: Efficient verification of timed automata with bdd-like data-structures. In: VMCAI 2003. Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, London, UK, pp. 189–205. Springer-Verlag, Heidelberg (2003)
Yan, R., Li, G., Tang, Z.: Symbolic model checking of finite precision timed automata. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 272–287. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 IFIP International Federation for Information Processing
About this paper
Cite this paper
Yan, R., Li, G., Zhang, W., Peng, Y. (2007). Improvements for the Symbolic Verification of Timed Automata. In: Derrick, J., Vain, J. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2007. FORTE 2007. Lecture Notes in Computer Science, vol 4574. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73196-2_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-73196-2_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73195-5
Online ISBN: 978-3-540-73196-2
eBook Packages: Computer ScienceComputer Science (R0)