Towards an Automatic Translation of Colored Petri Nets to Maude Language

Authors: Noura Boudiaf, Abdelhamid Djebbar

Abstract:

Colored Petri Nets (CPN) are very known kind of high level Petri nets. With sound and complete semantics, rewriting logic is one of very powerful logics in description and verification of non-deterministic concurrent systems. Recently, CPN semantics are defined in terms of rewriting logic, allowing us to built models by formal reasoning. In this paper, we propose an automatic translation of CPN to the rewriting logic language Maude. This tool allows graphical editing and simulating CPN. The tool allows the user drawing a CPN graphically and automatic translating the graphical representation of the drawn CPN to Maude specification. Then, Maude language is used to perform the simulation of the resulted Maude specification. It is the first rewriting logic based environment for this category of Petri Nets.

Keywords: Colored Petri Nets, Rewriting Logic, Maude, Graphical Edition, Automatic Translation, Simulation.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1070647

References:

[1] D. Basin, M. Clavel, and J. Meseguer, "Rewriting logic as a metalogical framework". In S. Kapoor and S. Prasad, editors, FST TCS 2000, pages 55-80. Springer LNCS, 2000.
[2] M. Beaudouin-Lafon and al., "CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets - ETAPS Tool Demonstration Related to TACAS". In: LNCS 2031: Tools and Algorithms for the Construction and Analysis of Systems, pages 574-pp. Springer Verlag, 2001.
[3] N. Boudiaf, "Développement des Outils Basés Maude pour les ECATNets. Domaine d-Application : Analyse des Programmes Ada,". Phd Thesis, University of Constantine, 2007.
[4] M. Clavel and aL," Maude Manual (Version 2.2)", Internal report, SRI International, December 2007.
[5] Francisco Durán, "Coherence Checker and Completion Tools for Maude Specifications". Manuscript. University of Málaga. July 2000.
[6] J. Meseguer, ''Rewriting Logic as a Semantic Framework of Concurrency: a Progress Report", Springer-Verlag, Lecture Notes in Computer Science, 119, pp. 331-372, 1996.
[7] J. Meseguer, "Rewriting logic and Maude: a Wide-Spectrum Semantic Framework for Object-based Distributed Systems", In S. Smith and C.L. Talcott, editors, Formal Methods for Open Object-based Distributed Systems, (FMOODS-2000), p. 89-117, 2000.
[8] Mark-Oliver Stehr, José Meseguer, Peter Csaba, "Rewriting Logic as a Unifying Framework for Petri Nets", Lecture Notes in Computer Science, volume 2128, 2001.
[9] Meta Software Corporation., "Design/CPN Tutorial for X-Windows : Version 2.0", Cambridge, England, 1993. http://www.daimi.au.dk/designCPN/man/
[10] L. Wells, "CPN-Tools : Computer Tool for Coloured Petri Nets" , Version 2, Fri 06 Dec 2002 Department of Computer Science University of Aarhus, Denmark, 2002. http://www.daimi.au.dk/CPNTools/