Abstract
In this paper, we present a framework for specifying and verifying an important class of hardware systems. These systems are build up from a parallel composition of circuits switching by a global clock. They can equivalently be characterised by Petri nets with a maximal step semantics. As a semantic model for these systems we introduce Distributed Synchronous Transition Systems (DSTS) which are distributed transition systems with a global clock synchronising the executions of actions. We show the relations to asynchronous behaviour of distributed transition systems emplyoing Mazurkiewicz trace theory which allows a uniform treatment of synchronous as well as asynchronous executions. We introduce a process algebra like calculus for defining DSTS which we call Synchronous Process Systems. Furthermore, we present Foata Lineartime Temporal Logic (FLTL) which is a temporal logic with a flavour of LTL adapted for specifying properties of DSTS. Our important contributions are the developed decision procedures for satisfiability as well as model checking of FLTL formulas, both based on alternating Büchi automata.
Actions lasting for more than one tick can be modelled by a sequence of single-tick actions.
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.
Similar content being viewed by others
References
S. Bensalem, P. Caspi, C. Parent-Vigouroux, and C. Dumas. A methodology for proving control systems with Lustre and PVS. In Charles B. Weinstock and John Rushby, editors, Dependable Computing for Critical Applications—7, volume 12 of Dependable Computing and Fault Tolerant Systems, pages 89–107, San Jose, CA, January 1999. IEEE Computer Society.
J. A. Brzozowski and E. Leiss. On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science, 10:19–35, 1980.
Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, January 1981. 198 Martin Leucker
P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. LUSTRE: A declarative language for programming synchronous systems. In Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, pages 178–188, Munich, West Germany, January 21-23, 1987. ACM SIGACT-SIGPLAN, ACM Press.
Volker Diekert and Yves Métivier. Partial commutation and traces. Technical Report TR-1996-02, Universität Stuttgart, Fakultät Informatik, Germany, March 1996.
Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.
M. Lange, M. Leucker, T. Noll, and S. Tobies. Truth — a verification platform for concurrent systems. In Tool Support for System Specification, Development, and Verification, Advances in Computing Science. Springer-Verlag Wien New York, 1999.
R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25(3):267–310, July 1983.
R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.
Motorola, editor. The PowerPC (TM) 601 User’s Manual. Motorola, 1993.
Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, 1992.
Doron Peled. Ten years of partial order reduction. In CAV, Computer Aided Verification, number 1427 in LNCS, pages 17–28, Vancouver, BC, Canada, 1998. Springer.
Doron Peled and Wojciech Penczek. Using asynchronous buchi automata for efficient model-checking of concurrent systems. In Protocol Specification Testing and Verification, pages 90–100, Warsaw, Poland, 1995. Chapman & Hall.
Wolfgang Reisig. Petrinetze. Springer-Verlag, Berlin Heidelberg New York Tokyo, 2 edition, 1986.
P. S. Thiagarajan and J. G. Henriksen. Distributed versions of linear time temporal logic: A trace perspective. Lecture Notes in Computer Science, 1492:643–681, 1998.
P. S. Thiagarajan. A trace consistent subset of PTL. In Insup Lee and Scott A. Smolka, editors, CONCUR’ 95: Concurrency Theory, 6th International Conference, volume 962 of Lecture Notes in Computer Science, pages 438–452, Philadelphia, Pennsylvania, 21-24 August 1995. Springer-Verlag.
Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133–191. Elsevier Science Publishers B. V., 1990.
Moshe Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic, volume 1043 of Lecture Notes in Computer Science, pages 238–266. Springer-Verlag Inc., New York, NY, USA, 1996.
WiesMlaw Zielonka. Notes on finite asynchronous automata. R.A.I.R.O. — Informatique Théorique et Applications, 21:99–135, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leucker, M. (2000). On Model Checking Synchronised Hardware Circuits. In: Jifeng, H., Sato, M. (eds) Advances in Computing Science — ASIAN 2000. ASIAN 2000. Lecture Notes in Computer Science, vol 1961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44464-5_14
Download citation
DOI: https://doi.org/10.1007/3-540-44464-5_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41428-5
Online ISBN: 978-3-540-44464-0
eBook Packages: Springer Book Archive