Formal Methods for Manufacturing Systems Control Design

The aim of this thesis is to propose a formal methodology for the design and verification of industrial control systems, with particular regard to the domain of manufacturing machines. The methodology is driven by an approach derived from Software Engineering concepts and is supported by the definition of a set of specification languages, derived from the semi-formal notation of UML [UML01], that permit to describe all the aspects related to the design of a complete machine control system, both architectural and behavioral. In particular, the underlying approach of the development process is oriented to the modularization and encapsulation of control tasks, in order to obtain a system architecture composed of independent and reusable components, as is suggested by Object-Oriented design techniques. Because of the hybrid nature of Manufacturing Systems, the control system may be partitioned into logic control modules and continuous control modules. Ideally, the architecture specification language proposed in this thesis would permit to describe both kind of components, together with their interactions. However, since the proposed methodology is mainly oriented to the solution of logic control problems, which are those less supported by formal methods in the industrial practice, the behaviour specification language adopted, derived from Statecharts [Har87], is basically event-oriented, with extensions that permit the description of simple data-processing operations. With regard to behavioral design, the suggested approach is that of direct design, which means that operational specifications on the desired behaviour of the manufacturing machine (or its components) are explicitly mapped into an operational model for each control module defined in the architecture specification. Formal verification of the control system design model can be performed, by means of a translation into a formal language. In particular, the technique suggested is model checking, in order to prove desired properties expressed in a form of temporal logic. For example, a model checking tool that can serve the purpose is SMV [McM93], which uses the temporal logic dialect CTL [CA81]. The rest of the thesis is organized as follows: - Chapter 2 presents a review of the most important formalisms and techniques to model and control Discrete Event Systems, with particular regard to their applicability in the manufacturing industry. - Chapter 3 describes a number of Software Engineering techniques that have been successfully applied to the domain of Real-Time software design, even if they are principally supported by semiformal languages. In particular, the techniques adopting Statecharts for behavioral specification are described in depth and with emphasis on the different semantical interpretations. - Chapter 4 describes the design methodology for industrial control systems proposed by this thesis, including the underlying approach, the specification languages adopted and the relationships with the features of the application domain. - Chapter 5 presents the definition of formal procedures to verify the correctness of industrial control systems, designed and modeled with the methods proposed in Chapter 4, and briefly describes how the design models can be implemented on real controllers. - Chapter 6 summarizes the features of the proposed approach to Manufacturing Systems control design, that aim to introduce the use of formal methods in the industrial practice, and ends with proposals for future work. - The thesis ends with an illustrative example of control system design and verification, described in Appendix A, referred to a machine component quite common in the packaging industry.