A Maude Implementation of Rewritable Petri Nets: a Feasible Model for Dynamically Reconfigurable Systems
This work addresses the need for more expressive models in concurrent or distributed systems, particularly for dynamic reconfiguration, though it appears incremental as it builds on existing formal methods.
The authors tackled the problem of modeling dynamically reconfigurable systems by proposing a Maude implementation of rewritable Petri nets, which combines Petri nets with rewriting logic to enhance expressiveness for dynamic reconfiguration, as demonstrated through a fault-tolerant manufacturing system example.
Petri Nets (PN) are a central, theoretically sound model for concurrent or distributed systems but, at least in their classical definition, not expressive enough to represent dynamic reconfiguration capabilities. On the other side, Rewriting Logic has proved to be a natural semantic framework for several formal models of concurrent/distributed systems. We propose a compact, efficient Maude formalization of dynamically reconfigurable PT nets (with inhibitor arcs), using as a running example the specification of a simple, fault-tolerant manufacturing system. We discuss the advantages of such a combined approach, as well as some concerns that it raises.