Skip to main content
SpringerLink
Log in

On Model Checking Synchronised Hardware Circuits

  • Conference paper
  • First Online:
Advances in Computing Science — ASIAN 2000 (ASIAN 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1961))

Included in the following conference series:

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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.

    Google Scholar 

  2. J. A. Brzozowski and E. Leiss. On equations for regular languages, finite automata, and sequential networks. Theoretical Computer Science, 10:19–35, 1980.

    Article  MATH  MathSciNet  Google Scholar 

  3. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114–133, January 1981. 198 Martin Leucker

    Article  MATH  MathSciNet  Google Scholar 

  4. 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.

    Google Scholar 

  5. Volker Diekert and Yves Métivier. Partial commutation and traces. Technical Report TR-1996-02, Universität Stuttgart, Fakultät Informatik, Germany, March 1996.

    Google Scholar 

  6. Volker Diekert and Grzegorz Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25(3):267–310, July 1983.

    Article  MATH  MathSciNet  Google Scholar 

  9. R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989.

    Google Scholar 

  10. Motorola, editor. The PowerPC (TM) 601 User’s Manual. Motorola, 1993.

    Google Scholar 

  11. Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer, New York, 1992.

    Google Scholar 

  12. 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.

    Chapter  Google Scholar 

  13. 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.

    Google Scholar 

  14. Wolfgang Reisig. Petrinetze. Springer-Verlag, Berlin Heidelberg New York Tokyo, 2 edition, 1986.

    Google Scholar 

  15. 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.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. 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.

    Google Scholar 

  18. 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.

    Google Scholar 

  19. WiesMlaw Zielonka. Notes on finite asynchronous automata. R.A.I.R.O. — Informatique Théorique et Applications, 21:99–135, 1987.

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. RWTH AachenLehrstuhl für Informatik II, Ahornstr. 55, D-52074, Aachen, Germany

    Martin Leucker

Authors
  1. Martin Leucker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, Casa Silva Mendes,Estrada do Engenheiro Trigo NO 4, Macau, China

    He Jifeng

  2. Graduate School of Informatics, Kyoto University, 606-8501, Kyoto, Sakyo-ku, Japan

    Masahiko Sato

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation