CIRTA: A FORMAL LANGUAGE FOR MODULAR ECATNETS SPECIFICATION
Keywords:
Specification language, Petri nets, ECATNets, algebraic specification.Abstract
CIRTA (''Construction Incrémentale des Réseaux de Petri à Termes Algébriques”) is aspecification language endowing ECATNets (''Extended Concurrent Algebraic Terms Nets”) [6][10]
with modularity concepts to make them more suitable for real-world applications. This paper
addresses the structuring mechanisms provided by CIRTA, for the design of complex concurrent
systems. Two structuring techniques are presented. The first one relies on the usage of CIRTA
modules which extend ECATNets with the concepts of interface nodes and composed-nodes. The
second mechanism concerns with some structuring operations on CIRTA modules namely:
importation, composition and renaming. The semantics of each CIRTA specification using these
constructs is defined by giving the behavioral equivalent ECATNet.
References
- L. Lavagro, A. Sangiovanni-Vicentilli, and E.
Sentovich, ''Models of Computation for Embedded
System Design'', in System-Level Synthesis, A.A.
Jerraya and J. Mermet, ed. Dordecht: Kluwer,1999,
pp.45-102.
P.Maciel, E. Barros, and W. Rosenstiel, '' A Petri net
Model for Hardware/Software codesign'', in Design
Automation for Embedded Systems, Vol.4, pp.243-310,
Oct.1999.
M.Varea, and B. Al-Hashimi, ''Dual Transitions Petri
Net Based Modelling Technique for Embedded
Systems Specification'', in Proc. DATE Conference,
, pp.566-571.
M.Sgroi, L. Lavagno, Y. Watanabe, and A.
Sangiovanni-Vincentelli, ''Synthesis of Embedded
Software Using Free-Choice Petri Nets'', in Proc. DAC,
, pp. 805-810.
M. Bettaz, M. Maouche ''Modelling of Object Based
Systems with hidden sorted ECATNets''. MASCOTS'
, Durham, North-Carolina, IEEE, 1995, pp.307-311.
M. Bettaz, M. Maouche, M. Soualmi, and M.
Boukebeche, ''Compact modelling and rapid
prototyping of communication software with
ECATNets: a case study''. Simulation Series Vol.25,
N°1, SCS 1993, pp149-154.
P. Borovansky, C.Kirchner, H. Kirchner, P6E. Moreau,
and M. Vittek. ''ELAN: A logical framework based on
computational systems''. Proc. first Intl. Workshop on
Rewriting Logic and its applications, Vol. 4 of
Electronic Notes in Theoretical Computer Science.
Elsevier, 1996.
M. Bettaz, G. Reggio ''A SMoLCS Based Kit for
Defining the Semantics of High Level Algebraic Petri
Nets'', LNCS 785, pp.98-112, Springer-Verlag, 1994.
M. Clavel, F. Duran, S. Eker, J. Meseguer, and M.-O.
Stehr. ''Maude as a Formal meta-tool''. In J. M. Wing,
J.Woodcock, and J. Davies, editors, Proc. FM'99,
LNCS 1709 , pp 1684-1703. Springer,1999.
K. Djemame, D.G. Gilles, L.M. Mackenzie, M. Bettaz,
''Performance comparison of high-level algebraic nets
distributed simulation protocols''. in Journal of systems
architecture 44 (1998) pp.457-472.
F. Belala ''Un cadre Formel pour l'Analyse des
ECATNets'' Thèse Dept. Informatique, Univ.
Constantine, 2002.
E. Pelz, and H. Fleishhack, ''Compositional high-level
Petri nets with timing constraints''. Third international
Conference on application of concurrency to system
design ACSD' 03, June 2003, Guimaraes, Portugal.
J.Meseguer. ''Rewriting Logic as a Semantic
Framework for Concurrency''. In U. Montanari and V.
Sassone, editors, Proc. Concur'96, Volume 1119 of
LNCS, pp.331-372, Springer, 1996.
J.Meseguer. ''Resarch Directions in Rewriting Logic''.
In U. Berger H. Schwichtenberg, editors, NATO ASI
Series F: Computer and Systems Sciences 165, pp 347-
Springer,1999.
K.Futatsugi and R. Diaconescu. ''CafeOBJ report''.
AMAST Series, World Scientific, 1998.
H. Fleishhack, and E. Pelz, ''Hierarchical timed high
level nets and their branching processes'', in
ICATPN'03, LNCS 2679, pp 397-416, Spinger, 2003.
Downloads
Published
How to Cite
Issue
Section
License
Les auteurs publiant dans cette revue acceptent les termes suivants :- Les auteurs détiennent le droit d'auteurs et accordent à la revue
le droit de première publication, avec l’ouvrage disponible simultanément [SPÉCIFIER LA PÉRIODE DE TEMPS] après publication, sous la licence Licence d’attribution Creative Commons qui permet à d'autres de partager l'ouvrage en en reconnaissant la paternité et la publication initiale dans cette revue. - Les auteurs peuvent conclure des ententes contractuelles additionnelles et séparées pour la diffusion non exclusive de la version imprimée de l'ouvrage par la revue (par ex., le dépôt institutionnel ou la publication dans un livre), accompagné d'une mention reconnaissant sa publication initiale dans cette revue.
- Les auteurs ont le droit et sont encouragés à publier leur ouvrage en ligne (par ex., dans un dépôt institutionnel ou sur le site Web d'une institution) avant et pendant le processus de soumission, car cela peut mener à des échanges fructueux ainsi qu'à un nombre plus important, plus rapidement, de références à l’ouvrage publié (Consulter The Effect of Open Access).
