Cyber-physical automation systems modelling with IEC 61499 for their formal verification
Published in 2021 IEEE 19th International Conference on Industrial Informatics (INDIN), 2021
Recommended citation: M. Xavier, S. Patil, V. Vyatkin. "Cyber-physical automation systems modelling with IEC 61499 for their formal verification." 2021 IEEE 19th International Conference on Industrial Informatics (INDIN), 2021.
This paper introduces a problem-oriented notation within the IEC 61499 syntax to be used for creating formal closed-loop models of cyber-physical automation systems. The proposed notation enables creation of a comprehensive tool-chain that can combine design, simulation, formal verification and distributed deployment of automation software. The proposed notation allows for definition of non-deterministic transitions in ECC of basic function blocks of IEC 61499. The tool chain includes an IEC 61499 compliant engineering environment, fb2smv converter of functions blocks to SMV code, the NuSMV model-checker and utilities for interpreting counterexamples.