Reconfigurable systems have received much attention from academia and industry because they are efficient, agile, and reasonably priced, and they are the trend of all future systems. The chapter focuses on dynamic automatic reconfigurations of Control Systems to be classically modeled by Petri nets. Several modeling and verification methods for such systems are shown and compared before the introduction of the research work on feasible dynamic reconfigurations and the implementation of manufacturing systems based on Petri nets. Three different reconfiguration scenarios can be applied at run-time to such systems: Addition/Removal of places, Addition/Removal/Update of transitions, or finally, the simple modification of the initial marking. Three formal modules are defined accordingly, which allow the reconfigurations of the system’s Petri nets model: the first module to dynamically change places of the model, the second to dynamically reconfigure transitions within a given subset of places, and the third to modify the initial markings of places. To check the correct behavior of this architecture according to user requirements, the model checker SESA is applied for the verification of CTL-based properties of the proposed modules and also of the system. The contribution is applied to a real-world Benchmark Production System.
Top1. Introduction
Contemporary control systems are addressing new criteria as flexibility and agility. To reduce their cost, these systems should be changed and adapted to their inconstant marketing requirements and disturbed work environment without disturbances. Several interesting academic and industrial research works have been made in recent years to develop reconfigurable control systems (Gehin & Staroswiecki, 2008). We distinguish in these works two reconfiguration policies: static and dynamic. Static reconfigurations are applied off-line to apply changes before the system's cold start (Angelov, Sierszecki, & Marian, 2005), whereas dynamic reconfigurations are dynamically applied at run-time. Two cases exist in dynamic reconfiguration policy: manual reconfigurations applied by users (Rooker, Sunder, Strasser, Zoitl, Hummer, & Ebenhofer, 2007) and automatic reconfigurations applied by Intelligent Agents (Al-Safi & Vyatkin, 2007). We focus in this chapter in automatic reconfigurations of control systems that are modeled by the formalism Net Condition/Event Systems (NCES) that is an extension of Petri nets (Rausch & Hanisch, 1995). In NCES, places classically correspond to control actions to be done by the control system. To move or remove a token from a place to another, a transition should be fired. There are several conditions to be fulfilled to enable a transition to fire. First of all, all pre-places have to be marked with at least one token. In addition, it may have incoming condition arcs from places and event arcs from other transitions. A transition is enabled by condition signals if each of its source places is marked by at least one token. The other type of influence on the firing can be described by event signals that come to the transition from other transitions. We mean in this research study by an automatic reconfiguration any addition/removal of elements such as places, transitions, condition signals or event signals in/from the NCES model of the control system, and any update in the initial marking. To handle automatic reconfigurations, we define three types of NCES-based modules such that the first allows the addition-removal of places in/from the system's NCES, the second allows addition/removal of transitions, event signals, condition signals in-from the system within the given subset of places, and finally the third allows modifications of the initial marking. To check the correct behavior of the whole system after any reconfiguration scenario, a model checking is applied by using the tool SESA that allows verifications of properties of system's NCES and also of the proposed modules (Rausch & Hanisch, 1995). We use the temporal logic “Computation Tree Logic” (denoted by CTL) to specify these properties (Roch, 2000a, 2000b). The contribution is applied to a real-world Benchmark Production System EnAS developed in the Research Laboratory of Prof. and Dr. Hans-Michael Hanisch at Martin Luther University Halle-Wittenberg in Germany.
A quick state of the art on formal methods for reconfigurable control systems and model checkers are presented in the next section, before the description of the formalism Net Condition/Event Systems (NCES) in Section 3 and the presentation of the temporal logic Computation Tree Logic (CTL) as well as its extensions in Section 4. The Benchmark Production System EnAS to be followed as a running example in this chapter is presented in Section 5. The specification of reconfigurable control systems are shown in Section 6 and the reconfiguration modules are proposed in Section 7. The model checking of the whole architecture is applied in Section 8. Finally, the last concludes this chapter.