Skip to main content
SpringerLink
Log in

Implementing Model Checking and Equivalence Checking for Time Petri Nets by the RT-MEC Tool

  • Conference paper
  • First Online:
Parallel Computing Technologies (PaCT 1999)

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

Included in the following conference series:

Abstract

RT-MEC is a tool box for validation (via graphical simulation) and verification (via model checking and equivalence checking) of real time systems based on partial order reduction [11] and on-the-fly technique [10]. It is appropriate for systems that can be modelled as Petri nets with real (dense) time. The tool is available within the system PEP (Programming Environment based on Petri nets) [4]. In this note, we present the RT-MEC tool, including general unique features, and summarize our development and usage experience.

This work is partially supported by the Russian State Committee of High Education for Basic Research in Mathematics.

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. R. Alur, C. Courcoubetis, D. Dill. Model-Checking for Real-Time Systems. In Proceedings of 5th Symposium on Logic in Computer Science (LICS’90), pages 414–425, 1990.

    Google Scholar 

  2. R. Alur, R. P. Kurshan. Timing Analysis in Cospan. Volume 1066 of Lecture Notes in Computer Science, pages 220–231, 1996.

    Google Scholar 

  3. J. R. Burch, E. M. Clarke, L. McMillan, D. Dill, J. Hwang. Symbolic Model Checking: 1020 and Beyond. In Proceedings of the 5th Symposium on Logic in Computer Science (LICS’90), pages 428–439, 1990.

    Google Scholar 

  4. E. Best, B. Grahlmann. PEP — More Than a Petri Net Tool. Volume 1055 of Lecture Notes in Computer Science, pages 397–401, 1996.

    Google Scholar 

  5. B. Berthomieu, M. Menasche. A State Enumeration Approach for Analyzing Time Petri Nets. Proceedings of the 3th European Workshop on Application and Theory of Petri Nets, pages 27–65, 1982.

    Google Scholar 

  6. E. M. Clarke, D. E. Long, K. L. Mc Millan. Compositional Model Checking Proceedings of the 4th Symposium on Logic in Computer Science (LICS’89), pages 353–362, 1990.

    Google Scholar 

  7. E. Emersen, A. Sistla. Symmetry and Model Checking. Volume 697 of Lecture Notes in Computer Science, pages 463–478, 1993.

    Google Scholar 

  8. J. Esparza. Model Checking Using Net Unfoldings. Science of Computer Programming, 23:151–195, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  9. F. Feldbrugge. Petri Net Tools Overview 1992. Volume 674 of Lecture Notes in Computer Science, pages 169–209, 1993.

    Google Scholar 

  10. J.-C. Fernandez, L. Mounier. ‘On the fly’ Verification of Behavioral Equivalences and Preorders. Volume 577 of Lecture Notes in Computer Science, pages 181–191, 1991.

    Google Scholar 

  11. P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems. An Approach for State-Explosion Problem. Volume 1032 of Lecture Notes in Computer Science, pages 1–143, 1996.

    Google Scholar 

  12. T. A. Henzinger, P. H. Ho, H. Wong-Toi. A Model Checking for Hybrid Systems. Volume 1254 of Lecture Notes in Computer Science, pages 220–231, 1997.

    Google Scholar 

  13. F. Laroussenie, K. G. Larsen. CMC: a Tool for Compositional Model Checking of Real-time Systems. In Proceedings of FORTE XI/PSTV XVIII’98, November 1998, Paris, France, pages 439–456, 1998.

    Google Scholar 

  14. K. G. Larsen, P. Pettersson, W. Yi. UPPAAL: Status and Developments. Volume 1254 of Lecture Notes in Computer Science, pages 456–459, 1997.

    Google Scholar 

  15. P. Merlin, D. J. Faber. Recoverability of Communication Protocols: Implications of a Theoretical Study. IEEE Trans. of Commun., COM-24(9):1036–1043, 1976.

    Article  Google Scholar 

  16. J.-L. Roux, B. Berthomieu. Verification of Local Area Network Protocol with Tine, a Software Package for Time Petri Nets. In Proceedings of the 7th European Workshop on Application and Theory of Petri Nets, pages 183–205, 1986.

    Google Scholar 

  17. P. Starke. INA: Integrated Net Analyzer. Handbuch, 1992. 198

    Google Scholar 

  18. H. Störrle. Tool Comparison, to be published, 1998. 195

    Google Scholar 

  19. I. B. Virbitskaite, E. A. Pokozy. A Partial Order Algorithm for Verifying Time Petri Nets. In Proceedings of International Workshop on Discrete Event Systems (WoDES’98), August 1998, Cagliari, Italy, IEE Publisher, London, pages 514–517, 1998.

    Google Scholar 

  20. I. B. Virbitskaite, E. A. Pokozy. Parametric Behaviour Analysis for Time Petri Nets (see this volume).

    Google Scholar 

  21. I. B. Virbitskaite, I. V. Tarasyuk. Equivalence Notions and Refinement for Time Petri Nets. Volume 8 of Joint Bulletin of NCC and IIS, Series Computer Science, Novosibirsk, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Siberian Division of the Russian Academy of Sciences, Institute of Informatics Systems, 6, Acad. Lavrentiev av., 630090, Novosibirsk, Russia

    A.V. Bystrov & I.B. Virbitskaite

Authors
  1. A.V. Bystrov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. I.B. Virbitskaite
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Center, 6 Lavrentiev Avenue, Novosibirsk, 630090, Russia

    Victor Malyshkin

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bystrov, A., Virbitskaite, I. (1999). Implementing Model Checking and Equivalence Checking for Time Petri Nets by the RT-MEC Tool. In: Malyshkin, V. (eds) Parallel Computing Technologies. PaCT 1999. Lecture Notes in Computer Science, vol 1662. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48387-X_20

Download citation

  • DOI: https://doi.org/10.1007/3-540-48387-X_20

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66363-8

  • Online ISBN: 978-3-540-48387-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation