Verification of Reconfigurable Petri Nets
We introduce a family of modeling techniques consisting of Petri nets together with a set of rules. For reconfigurable Petri nets not only the follower marking can be computed but also the structure can be changed by rule application to obtain a new net. Motivation is the observation that in increasingly many application areas the underlying system has to be dynamic in a structural sense. coordination and structural adaptation at run-time (e.g. mobile ad-hoc networks, dynamic hardware reconfiguration, communication spaces, ubiquitous computing) are main features that need to be modelled adequately. The distinction between the net behaviour and the dynamic change of its net structure is the characteristic feature that makes reconfigurable Petri nets so suitable for systems with dynamic structures.
For rule-based modification of Petri nets we use the framework of net transformations that is inspired by graph transformation systems. The basic idea behind net transformation is the stepwise modification of Petri nets by given rules. The rules present a rewriting of nets where the left-hand side is replaced by the right-hand side.
The abstract semantics we introduce is a graph with nodes that consist of an isomorphism class of the net structure and an isomorphism class of the current marking. Arcs between these nodes represent computation steps being either a transition firing or a direct transformation. Based on this semantics we can define properties and model-check these properties.
Model checking is a widely used technique to prove properties such as liveness, deadlock or safety for a given model. Here we introduce model checking of reconfigurable Petri nets. The main task is to flatten the two levels of dynamic behavior that reconfigurable nets provide, the firing of transitions on the one hand and the transformation of the nets on the other hand. We show how to translate a reconfigurable net into Maude modules. Maude's LTL model-checker is then used to verify properties of these modules. The correctness of this conversion is proves as the corresponding labelled transitions systems are bisimular.
In an ongoing example reconfigurable Petri nets are used to model and to verify partial dynamic reconfiguration of field programmable gate arrays.