Abstract
This paper proposes a partial order reduction algorithm for timed trace theoretic verification in order to detect both safety failures and timing failures of timed circuits efficiently. This algorithm is based on the framework of timed trace theoretic verification according to the original untimed trace theory. Consequently, its conformance checking supports hierarchical verification. Experimenting with the STARI circuits, the proposed approach shows its effectiveness.
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
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) APN 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991)
Godefroid, P.: Using partial orders to improve automatic verification methods. In: Proc. of Computer Aided Verification Workshop (1990)
Katz, S., Peled, D.: Defining conditional independence using collapses. Semantics for concurrency. In: Kwiatkowska, M. (ed.) BCS-FACS Workshop, Springer, Heidelberg (1990)
McMillan, K.L.: Trace theoretic verification of asynchronous circuits using unfoldings. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 180–195. Springer, Heidelberg (1995)
Mercer, E.G.: Correctness and Reduction in Timed Circuit Analysis. PhD thesis, Universty of Utah (2002)
Yoneda, T., Ryu, H.: Timed trace theoretic verification using partial order reduction. In: Proc. of Fifth International Symposium on Advanced Research in Asynchronous Circuits and Systems, pp. 108–121 (1999)
Zhou, B., Yoneda, T., Schlingloff, H.: Conformance and mirroring for timed asynchronous circuits. In: Proc. of ASP-DAC 2001, pp. 341–346 (2001)
Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, Cambridge (1988)
Zhou, B., Yoneda, T.: Verification of asynchronous circuits with bounded delay model. IEICE Trans. J82-D-I(7), 819–833 (1999)
Tasiran, S., Brayton, R.: 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)
Belluomini, W., Myers, C.: Verification of timed systems using POSETs. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 403–415. Springer, Heidelberg (1998)
Minea, M.: Partial order reduction for verification of timed systems. PhD thesis, Carnegie Mellon University (1999)
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
Pradubsuwun, D., Yoneda, T., Myers, C. (2004). Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive