A Maude Implementation of Rewritable Petri Nets: a Feasible Model for Dynamically Reconfigurable Systems

Lorenzo Capra
(Dipartimento di Informatica, Università degli Studi di Milano)

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.

In Mario Gleirscher, Jaco van de Pol and Jim Woodcock: Proceedings First Workshop on Applicable Formal Methods (AppFM 2021), virtual, 23rd November 2021, Electronic Proceedings in Theoretical Computer Science 349, pp. 31–49.
Published: 16th November 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.349.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org