Formal verification for analysis and design of logic controllers for reconfigurable machining systems

We present a hierarchical structure and framework for the modeling, specification, analysis and design of logic controllers for a reconfigurable machining system (RMS). This hierarchical framework allows one to integrate controllers at various levels of coordination in the machining system. Our approach is modular and "object oriented." This allows reusability and rapid reconfigurability of the controller as the machining system is reconfigured. We utilize the concept of timed transition models (TTM) 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). In this framework, the controller analysis problem can be posed as the problem of verifying that certain logical formulae are valid. Such verification can be carried out using either theorem proving techniques or model checking. 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. The paper also illustrates how the state explosion problem inherent in model checking can be handled effectively by performing modular verification.