Model-Checking based Verification approach for advanced Industrial Automation solutions

Modern automation systems shall be able to conjugate increasing complexity of controlled processes with agile production reconfiguration requirements. In such a context, structured design approaches based on formal reference models as well as integrated verification and validation process, have to be adopted. To such an aim, present paper proposes an approach based on Model-Checking methods and tools oriented to the Verification of logic control systems in the field of Industrial Automation. In particular, graphical Stateflow based model deployment, Bounded Model Checking techniques and Model Coverage properties have been considered. Furthermore, the proposed approach have been applied regarding the development of the control solution for an automatic warehouse system integrated into a flexible shoes manufacturing plant.