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

Abstract

In this dissertation, we present a novel framework for the modeling, specification, analysis and design of logic controllers for Reconfigurable Manufacturing Systems (RMS). This framework allows one to integrate controllers at various levels of coordination in the manufacturing system. Our approach is modular and object oriented. This allows reusability and rapid reconfigurability of the controller as the manufacturing system is reconfigured. We utilize the concept of timed transition models (TTM) introduced by Ostroff to model an RMS. We also model the underlying OS mechanisms such as message passing, process scheduling, etc. as TTMs. To specify the desired functional and temporal behavior of the RMS, we use Real Time Temporal Language (RTTL) introduced by Manna and Pnueli. 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 or model checking techniques. We present some analytical results on a problem of system reconfiguration. An iterative approach for designing a controller based on repeated verification 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. We present an analysis methodology based on simulation of the real-time behavior of the final system to elucidate some high level system deadlock issues introduced by the underlying operating system. This dissertation also illustrates how the state explosion problem inherent in model-checking can be handled effectively by performing modular verification. We present a CAD tool SF2STeP that allows us to model a TTM in Stateflow and verify the correctness of the Stateflow diagram using the formal verification tool STeP. We also present a CAD tool SF2C++ that allows us to generate executable C++ code from a Stateflow model of the logic controller(s). Methods introduced in this dissertation have been successfully implemented on a small-scale test bed in the NSF Engineering Center for Reconfigurable Machining Systems.