Abstract
In this paper we report some progress in applying timed automata technology to large-scale problems. We focus on the problem of finding maximal stabilization time for combinational circuits whose inputs change only once and hence they can be modeled using acyclic timed automata. We develop a “divide-and-conquer” methodology based on decomposing the circuit into sub-circuits and using timed automata analysis tools to build conservative low-complexity approximations of the sub-circuits to be used as inputs for the rest of the system. Some preliminary results of this methodology are reported.
This work was partially supported by a grant from Intel and by the European Community Projects IST-2001-35304 AMETIST (Advanced Methods for Timed Systems), http://ametist.cs.utwente.nl
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
Alur, R.: Timed Automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Itai, A., Kurshan, R.P., Yanakakis, M.: Timing Verification by Successive Approximation. Information and Computation 118, 142–157 (1995)
Balarin, F.: Approximate Reachability Analysis of Timed Automata. In: Proc. RTSS 1996, pp. 52–61. IEEE, Los Alamitos (1996)
Bozga, M., Graf, S., Mounier, L.: IF-2.0: A Validation Environment for Component-Based Real-Time Systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 343. Springer, Heidelberg (2002)
Dill, D.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, Springer, Heidelberg (1990)
Bozga, M., Fernandez, J.-C., Kerbrat, A., Mounier, L.: Protocol Verification with the Aldebaran Toolset. Software Tools for Technology Transfer 1, 166–183 (1997)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a Model-Checking Tool for Real-Time Systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, Springer, Heidelberg (1998)
Bozga, M., Jianmin, H., Maler, O., Yovine, S.: Verification of Asynchronous Circuits using Timed Automata. ENTCS, vol. 65 (2002)
Bouajjani, A., Fernandez, J.-C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, Springer, Heidelberg (1991)
Bozga, M., Maler, O., Pnueli, A., Yovine, S.: Some Progress in the Symbolic Verification of Timed Automata. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 179–190. Springer, Heidelberg (1997)
Bozga, M., Maler, O., Tripakis, S.: Efficient Verification of Timed Automata using Dense and Discrete Time Semantics. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 125–141. Springer, Heidelberg (1999)
Brzozowski, J.A., Seger, C.-J.H.: Asynchronous Circuits. Springer, Heidelberg (1994)
Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic Modelchecking for Real-time Systems. Information and Computation 111, 193–244 (1994)
Lewis, H.R.: Finite-state Analysis of Asynchronous Circuits with Bounded Temporal Uncertainty, TR15-89, Harvard University (1989)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Software Tools for Technology Transfer 1/2 (1997)
Maler, O., Pnueli, A.: Timing Analysis of Asynchronous Circuits using Timed Automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 189–205. Springer, Heidelberg (1995)
Maler, O., Yovine, S.: Hardware Timing Verification using KRONOS. In: Proc. 7th Israeli Conference on Computer Systems and Software Engineering (1996)
Pena, M.A., Cortadella, J., Kondratyev, A., Pastor, E.: Formal Verification of Safety Properties in Timed Circuits. In: Proc. Async 2000, pp. 2–11. IEEE Press, Los Alamitos (2000)
Tasiran, S., Alur, R., Kurshan, R.P., Brayton, R.: Verifying Abstractions of Timed Systems. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 546–562. Springer, Heidelberg (1996)
Tasiran, S., Brayton, R.K.: STARI: A Case Study in Compositional and Hierarchical Timing Verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 191–201. Springer, Heidelberg (1997)
Tasiran, S., Kukimoto, Y., Brayton, R.K.: Computing Delay with Coupling using Timed Automata. In: Proc. TAU 1997 (1997)
Tasiran, S., Khatri, S.P., Yovine, S., Brayton, R.K., Sangiovanni- Vincentelli, A.: A Timed Automaton-Based Method for Accurate Computation of Circuit Delay in the Presence of Cross-Talk. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 149–166. Springer, Heidelberg (1998)
Wong-Toi, H., Dill, D.L.: Approximations for Verifying Timing Properties. In: Theories and Experiences for Real-Time System Development, World Scientific Publishing, Singapore (1994)
Yovine, S.: Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1 (1997)
Zheng, H., Mercer, E., Myers, C.: Modular Verification of Timed Circuits using Automatic Abstraction. IEEE Trans. on CAD (2003) (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salah, R.B., Bozga, M., Maler, O. (2004). On Timing Analysis of Combinational Circuits. In: Larsen, K.G., Niebert, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2003. Lecture Notes in Computer Science, vol 2791. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40903-8_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-40903-8_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21671-1
Online ISBN: 978-3-540-40903-8
eBook Packages: Springer Book Archive