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.