Formal verification for analysis and design of reconfigurable controllers for manufacturing systems

We present a hierarchical structure and framework for the representation, analysis and design of controllers for a reconfigurable machining system (RMS). This hierarchical framework allows one to integrate controllers at various levels of coordination in the manufacturing system. Our approach is modular and “object oriented”. This allows re-usability and rapid reconfigurability of the controller as the manufacturing system is reconfigured. In this paper, we utilize the concept of timed transition models introduced by Ostroff (1997) to model a RMS. To specify the desired controlled behavior of the RMS, we use the tools of Real Time Temporal Language introduced by Manna and Pnueli (1995). We present some analytical results on a problem of system reconfiguration. An iterative approach for designing a controller based on the analysis result mentioned above is also presented. Using this approach, we can design a controller for a given set of closed loop properties which guarantees correctness of the closed loop system