Towards an Automatic Translation of Colored Petri Nets to Maude Language

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.

Authors:

• Noura Boudiaf
• Abdelhamid Djebbar

Keywords:

• Colored Petri Nets
• Rewriting Logic
• Maude
• Graphical Edition
• Automatic Translation
• Simulation.

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/