Formal Verification of IEC 61499 Function Block Networks using Interface Automata

Systems are often developed using modular approaches to leverage reusability of compo-nents. However, even when each component is proven to function correctly, the overallsystem may still exhibit unexpected behaviour due to the complex interactions betweencomponents. This challenge highlights the need for verification techniques that extendbeyond individual components. This thesis presents a generic approach to verify networksof IEC 61499 Function Blocks using Interface Automata. The proposed method uses thecomposition formalism for Interface Automata to create a formal representation of theentire network. By employing this technique, potential errors in communication betweenthe modelled Function Blocks can be identified and eliminated, effectively validatingwhether the suggested network is valid. Moreover, the approach introduces the conceptof extending Interface Automata to account for often desired ignorance of issued events,tailoring it to IEC 61499 Function Blocks. The final method is presented as pseudocode inAlgorithm 3. To evaluate the effectiveness of the approach, it was applied to a real-worldexample, the Capping Station, and the results presented.