Towards a Modelling Framework for Dynamically Reconfigurable Systems Using Maude (& Petri Nets)

Petri Nets (PN) are a central model for concurrent or distributed systems, but not expressive enough to represent dynamically reconfigurable systems. Rewriting Logic in turn has proved to be suitable framework for several formal models of distributed systems. This paper proposes an efficient Maude formalization of dynamically reconfigurable PT nets (with inhibitor arcs) using as a running example a fault-tolerant manufacturing system. The main intent is to show the advantages of such a hybrid modelling approach and to discuss about some concerns that are raised. This work may be seen as a preliminary step towards the definition of a Maude-based modelling framework for dynamically reconfigurable distributed systems.