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: 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.
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.
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 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 and its programming language Maude. Rewriting
logic is considered as one of very powerful logics in terms of
description, verification and programming of concurrent systems We
proposed previously a method for translating Ada-95 tasking
programs to ECATNets formalism (Ada-ECATNet) and we showed
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. We showed also previously how the
ECATNet formalism offers to Ada many validation and verification
tools like simulation, Model Checking, accessibility analysis and
static analysis. In this paper, we describe the implementation of our
translation of the Ada programs into ECATNets.