Abstract
In this paper, we extend the verification method based on the failure semantics of process algebra and the resulting trace theory by Dill et al. for bounded delay asynchronous circuits. We define a timed conformance relation between trace structures which allows to express both safety and responsiveness properties. In our approach, bounded delay circuits as well as their real-time properties are modelled by time Petri nets. We give an explicit state-exploration algorithm to determine whether an implementation conforms to a specification. Since for IO-conflict free specifications the conformance relation is transitive, this algorithm can be used for hierarchical verification of large asynchronous circuits. We describe the implementation of our method and give some experimental results which demonstrate its efficiency.
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
R. Alur and D. Dill: Automata for Modelling Real-time Systems; LNCS600: Real time: Theory in Practice, pp. 45–73, (1992).
W. Belluomini and C. Myers: Verification of Timed Systems Using POSETS Proc. Int. Conf. on Computer Aided Verification (CAV), Univ. of British Columbia, Vancouver, Canada (1998)
B. Berthomieu and M. Diaz: Modeling and Verification of Time Dependent Systems using Time Petri Nets; IEEE Trans. on Software Eng., 17(3):259–273, (1991).
D. Dill: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits; PH.D. Thesis, MIT press, (1988).
J.D. Garside, S. Temple, and R. Mehra: The AMULET2e Cache System; Proc. of the Second International Symposium of ASYNC, pp. 208–217 (1996).
F. Jahanian and A. Mok: A Graph-Theoretic Approach for Timing Analysis and its Implementation; IEEE Trans. Comput. C-36(8):961–975 (1987).
D. Muller and W. Bartke: A Theory of Asynchronous Circuits; Theory of Switching, Harvard University Press, Masachusetts (1959).
P. Merlin and D. Faber: Recoverability of Communication Protocols; IEEE Trans. on Communication, COM-24(9), (1976).
T. Rokicki: Representing and Modeling Digital Circuits; Ph.D Dissertation, Stanford University, (1993).
W. Shigetaka: On the Acceleration of Formal Verification Methods; Thesis, Tokyo Institute of Technology (1994).
L. Twele, B.-H. Schlingloff, H. Szczerbicka: Performability Analysis of an Avionics-Interface; IEEE Symp. on Man, Machine and Cybernetics; San Diego, (1998)
T. Yoneda, B-H. Schlingloff: Efficient Verification of Parallel Real-Time Systems; Journal of Formal Methods in System Design 11-2, pp. 187–215, (1997).
T. Yoneda, T. Yoshikawa: Using Partial Orders for Trace Theoretic Verification of Asynchronous Circuits; Proc. of the Second International Symposium of ASYNC (1996).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yoneda, T., Zhou, B., Schlingloff, BH. (1998). Verification of Bounded Delay Asynchronous Circuits with Timed Traces. In: Haeberer, A.M. (eds) Algebraic Methodology and Software Technology. AMAST 1999. Lecture Notes in Computer Science, vol 1548. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49253-4_7
Download citation
DOI: https://doi.org/10.1007/3-540-49253-4_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65462-9
Online ISBN: 978-3-540-49253-5
eBook Packages: Springer Book Archive