Abstract
The paper deals with dynamic automatic reconfigurations of Control Systems to be classically modelled by Petri nets. Three different forms can be applied at run-time to reconfigure such systems: Addition/Removal of places, Addition/Removal/Update of transitions or finally the simple change of the initial marking. We define three formal modules allowing reconfigurations of the system's Petri nets: changer_places to dynamically change places of the model, changer_transitions to dynamically reconfigure transitions, and changer_marking to modify the initial markings of places. To guarantee a correct behavior of this architecture according to user requirements, we apply a model checking by using the useful tool SESA for the verification of CTL-based properties of the proposed modules and also of the system. The paper is applied to a Real Benchmark Production System.