Towards user-friendly model checking of IEC 61499 systems with counterexample explanation

Funding Information: This work was supported, in part, by the H2020 project 1-SWARM co-funded by the European Commission (grant agreement: 871743) and by the Government of the Russian Federation under Grant 08-08. Publisher Copyright: © 2021 IEEE.Distributed automation systems design is getting increasingly popular as the systems become more complex and modular. The IEC 61499 automation architecture is seen as the main enabler of component software design for distributed automation systems. It requires novel approaches to integrated development environments (IDE) supporting the engineering of such component software systems. One important part of automation systems engineering is their verification and validation. The efficacy of verification is largely dependent on how seamlessly this process is integrated with the traditional development tools, such as editors, compilers and debuggers. This work presents a start of such a development, that automatizes the model checking process for IEC 61499 systems and provides a visual explanation of its results in the graphical development environment FBME.Peer reviewe