Design and verification of mechatronic object-oriented models for industrial control systems

The paper describes a methodological framework that aims to apply formal design and verification techniques in the development of industrial control systems, with particular regard to the domain of manufacturing machines. The methodology is based on an object-oriented approach, revisited in a mechatronic perspective, and is supported by the specification methods proposed by the UML language. This language, opportunely adapted to the application domain, permits to describe control system design models which are modular, reusable and independent from the implementation architecture. The implementation domain is taken into account only during the verification phase, in which it is necessary to identify a correct semantical interpretation according to the execution model of the computational platform. In particular, the different frameworks of the industrial standards IEC 61131-3 and IEC 61499 are considered and compared with each other. The paper shows that formal verification techniques can be applied to prove the correctness of the design specification or to guide its iterative refinement, thanks to a translation of the O-O model into the input language of the model checking tool SMV.