Abstract
Model checking timed systems through digitization is relatively easy, compared to zone-based approaches. The applicability of digitization, however, is limited mainly for two reasons, i.e., it is only sound for closed timed systems; and clock ticks cause state space explosion. The former is mild as many practical systems are subject to digitization. It has been shown that BDD-based techniques can be used to tackle the latter to some extent. In this work, we significantly improve the existing approaches by keeping the ticks simple in the BDD encoding. Taking advantage of the ‘simple’ nature of clock ticks, we fine-tune the encoding of ticks and are able to verify systems with many ticks. Furthermore, we develop a BDD library which supports not only encoding/verifying of timed state machines (through digitization) but also composing timed components using a rich set of composition functions. The usefulness and scalability of the library are demonstrated by supporting two languages, i.e., closed timed automata and Stateful Timed CSP.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berthomieu, B., Menasche, M.: An Enumerative Approach for Analyzing Time Petri Nets. In: IFIP Congress, pp. 41–46 (1983)
Dill, D.L.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
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: RTSS, pp. 2–13 (1997)
Henzinger, T.A., Manna, Z., Pnueli, A.: What Good Are Digital Clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)
Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005)
Tripakis, S.: Verifying Progress in Timed Systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999)
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient Emptiness Check for Timed Büchi Automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 148–161. Springer, Heidelberg (2010)
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)
Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., André, E.: Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP. ACM Transactions on Software Engineering and Methodology (2011) (to appear)
Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S., Liu, Y.: BDD-based Discrete Analysis of Timed Systems, http://www.comp.nus.edu.sg/%7Epat/bddlib/
Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic Model Checking with Partitioned Transistion Relations. In: VLSI, pp. 49–58 (1991)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Jin, X.L., Ma, H.D., Gu, Z.H.: Real-Time Component Composition Using Hierarchical Timed Automata. In: QSIC, pp. 90–99. IEEE (2007)
David, A., David, R., Möller, M.O.: From HUPPAAL to UPPAAL - A Translation from Hierarchical Timed Automata to Flat Timed Automata. Technical report, Department of Computer Science, University of Aarhus (2001)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall (1985)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009)
Liu, Y., Sun, J., Dong, J.S.: Developing Model Checkers Using PAT. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 371–377. Springer, Heidelberg (2010)
Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS, pp. 332–344. IEEE Computer Society (1986)
Wang, H., MacCaull, W.: Verifying Real-Time Systems using Explicit-time Description Methods. In: QFM. EPTCS, vol. 13, pp. 67–78 (2009)
Morbé, G., Pigorsch, F., Scholl, C.: Fully Symbolic Model Checking for Timed Automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 616–632. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S., Liu, Y. (2012). Improved BDD-Based Discrete Analysis of Timed Systems. In: Giannakopoulou, D., Méry, D. (eds) FM 2012: Formal Methods. FM 2012. Lecture Notes in Computer Science, vol 7436. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32759-9_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-32759-9_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32758-2
Online ISBN: 978-3-642-32759-9
eBook Packages: Computer ScienceComputer Science (R0)