Abstract: One major difficulty that faces developers of
concurrent and distributed software is analysis for concurrency based
faults like deadlocks. Petri nets are used extensively in the
verification of correctness of concurrent programs. ECATNets [2] are
a category of algebraic Petri nets based on a sound combination of
algebraic abstract types and high-level Petri nets. ECATNets have
'sound' and 'complete' semantics because of their integration in
rewriting logic [12] and its programming language Maude [13].
Rewriting logic is considered as one of very powerful logics in terms
of description, verification and programming of concurrent systems.
We proposed in [4] a method for translating Ada-95 tasking
programs to ECATNets formalism (Ada-ECATNet). In this paper,
we show that ECATNets formalism provides a more compact
translation for Ada programs compared to the other approaches based
on simple Petri nets or Colored Petri nets (CPNs). Such translation
doesn-t reduce only the size of program, but reduces also the number
of program states. We show also, how this compact Ada-ECATNet
may be reduced again by applying reduction rules on it. This double
reduction of Ada-ECATNet permits a considerable minimization of
the memory space and run time of corresponding Maude program.
Abstract: The Petri net tool INA is a well known tool by the
Petri net community. However, it lacks a graphical environment to
cerate and analyse INA models. Building a modelling tool for the
design and analysis from scratch (for INA tool for example) is
generally a prohibitive task. Meta-Modelling approach is useful to
deal with such problems since it allows the modelling of the
formalisms themselves. In this paper, we propose an approach based
on the combined use of Meta-modelling and Graph Grammars to
automatically generate a visual modelling tool for INA for analysis
purposes. In our approach, the UML Class diagram formalism is
used to define a meta-model of INA models. The meta-modelling
tool ATOM3 is used to generate a visual modelling tool according to
the proposed INA meta-model. We have also proposed a graph
grammar to automatically generate INA description of the
graphically specified Petri net models. This allows the user to avoid
the errors when this description is done manually. Then the INA tool
is used to perform the simulation and the analysis of the resulted INA
description. Our environment is illustrated through an example.
Abstract: To analyze the behavior of Petri nets, the accessibility
graph and Model Checking are widely used. However, if the
analyzed Petri net is unbounded then the accessibility graph becomes
infinite and Model Checking can not be used even for small Petri
nets. ECATNets [2] are a category of algebraic Petri nets. The main
feature of ECATNets is their sound and complete semantics based on
rewriting logic [8] and its language Maude [9]. ECATNets analysis
may be done by using techniques of accessibility analysis and Model
Checking defined in Maude. But, these two techniques supported by
Maude do not work also with infinite-states systems. As a category
of Petri nets, ECATNets can be unbounded and so infinite systems.
In order to know if we can apply accessibility analysis and Model
Checking of Maude to an ECATNet, we propose in this paper an
algorithm allowing the detection if the ECATNet is bounded or not.
Moreover, we propose a rewriting logic based tool implementing this
algorithm. We show that the development of this tool using the
Maude system is facilitated thanks to the reflectivity of the rewriting
logic. Indeed, the self-interpretation of this logic allows us both the
modelling of an ECATNet and acting on it.