Skip to main content
SpringerLink
Log in

The Model-Checking Kit

  • Conference paper
  • First Online:
Applications and Theory of Petri Nets 2003 (ICATPN 2003)

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

Included in the following conference series:

Abstract

The Model-Checking Kit [8] is a collection of programs which allow to model finite state systems using a variety of modelling languages, and verify them using a variety of checkers, including deadlock-checkers, reachability-checkers, and model-checkers for the temporal logics CTL and LTL [7].

http://www7.in.tum.de/gruppen/theorie/KIT/

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. ADVANCE — Advanced Validation Techniques for Telecommunication Protocols. http://verif.liafa.jussieu.fr/~haberm/ADVANCE/main.html.

    Google Scholar 

  2. E. Best and B. Grahlmann. PEP Documentation and User Guide 1.8. Universität Oldenburg, 1998.

    Google Scholar 

  3. E. Best and R. P. Hopkins. B(PN)2 — a Basic Petri Net Programming Notation. In PARLE’93, LNCS 694, pages 379–390. Springer, 1993.

    Google Scholar 

  4. M. Bozga, J.-C. Fernandez, L. Ghirvu, S. Graf, L. Mounier, J. P. Krimm, and J. Sifakis. The Intermediate Representation IF. Technical Report. Vérimag, 1998.

    Google Scholar 

  5. R. E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug. 1986.

    Article  Google Scholar 

  6. J. C. Corbett. Evaluating Deadlock Detection Methods, 1994.

    Google Scholar 

  7. E. A. Emerson. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, volume B, pages 997–1067. Elsevier Science Publishers B. V., 1990.

    Google Scholar 

  8. J. Esparza, C. Schröter, and S. Schwoon. The Model-Checking Kit. http://www7.in.tum.de/gruppen/theorie/KIT/.

    Google Scholar 

  9. B. Grahlmann, M. Möller, and U. Anhalt. A new Interface for the PEP-tool — Parallel Finite Automata. 2nd Workshop of Algorithms and Tools for Petri nets. Oldenburg, 1995.

    Google Scholar 

  10. B. Grahlmann, S. Römer, T. Thielke, B. Graves, M. Damm, R. Riemann, L. Jenner, S. Melzer, and A. Gronewold. PEP: Programming Environment Based on Petri Nets. Technical Report 14, Universität Hildesheim, May 1995.

    Google Scholar 

  11. M. Heiner and P. Deusen. Petri net based qualitative analysis — A case study. Technical report I-08/1995. Brandenburg Technische Universität Cottbus, 1995.

    Google Scholar 

  12. K. Heljanko. Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets. PhD thesis, Helsinki University of Technology, 2002.

    Google Scholar 

  13. G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.

    Google Scholar 

  14. V. Khomenko. CLP. http://www.cs.ncl.ac.uk/people/victor.khomenko/home.formal/tools/tools.html.

    Google Scholar 

  15. C. Lewerentz and T. Lindner. Case Study Production Cell. In Formal Development of Reactive Systems, LNCS 891. Springer, 1995.

    Google Scholar 

  16. A. J. Martin. Self-timed FIFO: An exercise in compiling programs into VLSI circuits. In From HDL Descriptions to Guruanteed Correct Circuit Designs, pages 133–153. Elsevier Science Publishers, 1986.

    Google Scholar 

  17. K. L. McMillan. Symbolic Model Checking — An approach to the state explosion problem. PhD thesis, Carnegie Mellon University, 1992.

    Google Scholar 

  18. K. L. McMillan. Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. In CAV’92, LNCS 663, pages 164–174. Springer, 1992.

    Google Scholar 

  19. M. Raynal. Algorithms For Mutual Exclusion, 1986.

    Google Scholar 

  20. O. Roig, J. Cortadella, and E. Pastor. Verification of Asynchronous Circuits by BDD-based Model Checking of Petri Nets. In ATPN’95, LNCS 935, pages 374–391. Springer, 1995.

    Google Scholar 

  21. A. Valmari. On-the-Fly Verification with Stubborn Sets. In CAV’93, LNCS 697, pages 397–408. Springer, 1993.

    Google Scholar 

  22. K. Varpaaniemi, J. Halme, K. Hiekkanen, and T. Pyssysalo. PROD Reference Manual. Technical Reports, B(13):1–56, Aug. 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institutsverbund Informatik, Universität Stuttgart, Stuttgart

    Claus Schröter, Stefan Schwoon & Javier Esparza

Authors
  1. Claus Schröter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Schwoon
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Javier Esparza
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Technology and Management, Eindhoven University of Technology, P.O. Box 513, 5600 MB, Eindhoven, The Netherlands

    Wil M. P. van der Aalst

  2. Computer Science Department Parallel Systems Group, University of Oldenburg, 26111, Oldenburg, Germany

    Eike Best

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schröter, C., Schwoon, S., Esparza, J. (2003). The Model-Checking Kit. In: van der Aalst, W.M.P., Best, E. (eds) Applications and Theory of Petri Nets 2003. ICATPN 2003. Lecture Notes in Computer Science, vol 2679. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44919-1_29

Download citation

  • DOI: https://doi.org/10.1007/3-540-44919-1_29

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40334-0

  • Online ISBN: 978-3-540-44919-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation