Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Complexity is the Only Constant: Trends in Computing and Their Relevance to Model Driven Engineering Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Model Checking Reconfigurable Petri Nets with Maude

verfasst von : Julia Padberg, Alexander Schulz

Erschienen in: Graph Transformation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Model checking is a widely used technique to prove properties such as liveness, deadlock or safety for a given model. Here we introduce model checking of reconfigurable Petri nets. These are Petri nets with a set of rules for changing the net dynamically. We obtain model checking by converting reconfigurable Petri nets to specific Maude modules and using then the LTLR model checker of Maude. The main result of this paper is the correctness of this conversion. We show that the corresponding labelled transitions systems are bisimular. In an ongoing example reconfigurable Petri nets are used to model and to verify partial dynamic reconfiguration of field programmable gate arrays.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Parallelism in AGREE Transformations
Nächstes Kapitel A Software Package for Chemically Inspired Graph Transformation
Fußnoten
1
ReConNet (see [16]) is the tool for modelling and simulating reconfigurable Petri nets saving them as an extension of PNML.
 
Literatur
1.
Andreu, D., Souquet, G., Gil, T.: Petri net based rapid prototyping of digital complex system. In: IEEE Computer Society Annual Symposium on VLSI, ISVLSI 2008, pp. 405–410. IEEE Computer Society (2008)
2.
Bae, K., Meseguer, J.: A rewriting-based model checker for the linear temporal logic of rewriting. Electron. Notes Theoret. Comput. Sci. 290, 19–36 (2012)CrossRefMATH
3.
Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
4.
Barbosa, P., Barros, J.P., Ramalho, F., Gomes, L., Figueiredo, J., Moutinho, F., Costa, A., Aranha, A.: SysVeritas: a framework for verifying IOPT nets and execution semantics within embedded systems design. In: Camarinha-Matos, L.M. (ed.) Technological Innovation for Sustainability. IFIP AICT, vol. 349, pp. 256–265. Springer, Heidelberg (2011)CrossRef
5.
Boudiaf, N., Djebbar, A.: Towards an automatic translation of colored Petri nets to Maude language. Int. J. Comput. Sci. Eng. 3(1), 253–258 (2009)
6.
Bukowiec, A., Doligalski, M.: Petri net dynamic partial reconfiguration in FPGA. In: Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2013. LNCS, vol. 8111, pp. 436–443. Springer, Heidelberg (2013)CrossRef
7.
Chama, W., Elmansouri, R., Chaoui, A.: Using graph transformation and Maude to simulate and verify UML models. In: 2013 International Conference on Technological Advances in Electrical, Electronics and Computer Engineering (TAEECE), pp. 459–464 (2013)
8.
Chen, C.K.: A Petri net design of FPGA-based controller for a class of nuclear I&C systems. Nucl. Eng. Des. 241(7), 2597–2603 (2011)CrossRef
9.
Doligalski, M., Bukowiec, A.: Partial reconfiguration in the field of logic controllers design. Int. J. Electron. Telecommun. 59(4), 351–356 (2013)CrossRef
10.
Ehrig, H., Hoffmann, K., Padberg, J., Prange, U., Ermel, C.: Independence of net transformations and token firing in reconfigurable place/transition systems. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol. 4546, pp. 104–123. Springer, Heidelberg (2007)CrossRef
11.
Ehrig, H., Padberg, J.: Graph grammars and Petri net transformations. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 496–536. Springer, Heidelberg (2004)CrossRef
12.
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. Electr. Notes Theor. Comput. Sci. 71, 162–187 (2002)CrossRefMATH
13.
Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 230–234. Springer, Heidelberg (2003)CrossRef
14.
Jamro, M., Rzonca, D., Rzasa, W.: Testing communication tasks in distributed control systems with sysml and timed colored Petri nets model. Comput. Ind. 71, 77–87 (2015)CrossRef
15.
Meseguer, J.: A logical theory of concurrent objects. In: Yonezawa, A. (ed.) Proceedings of OOPSLA/ECOOP 1990, pp. 101–115. ACM (1990)
16.
Padberg, J., Ede, M., Oelker, G., Hoffmann, K.: Reconnet: a tool for modeling and simulating with reconfigurable place/transition nets. ECEASST 54 (2012)
17.
Padberg, J., Schulz, A.: Towards model checking reconfigurable Petri nets using Maude. ECEASST 68 (2014)
18.
Richta, T., Janousek, V., Kocí, R.: Petri nets-based development of dynamically reconfigurable embedded systems. In: Moldt, D. (ed.) Petri Nets and Software Engineering (PNSE 2013), vol. 989, pp. 203–217. CEUR-WS.org (2013)
19.
20.
21.
Soto, E., Pereira, M.: Implementing a Petri net specification in a FPGA using VHDL. In: Design of Embedded Control Systems, pp. 167–174. Springer, New York (2005)
22.
Stehr, M.-O., Meseguer, J., Ölveczky, P.C.: Rewriting logic as a unifying framework for Petri nets. In: Ehrig, H., Juhás, G., Padberg, J., Rozenberg, G. (eds.) APN 2001. LNCS, vol. 2128, pp. 250–303. Springer, Heidelberg (2001)CrossRef
Metadaten
Titel
Model Checking Reconfigurable Petri Nets with Maude
verfasst von
Julia Padberg
Alexander Schulz
Copyright-Jahr
2016
Buch
Graph Transformation

Print ISBN: 978-3-319-40529-2

Electronic ISBN: 978-3-319-40530-8

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40530-8_4