Transformation of Function Block Diagrams to UPPAAL Timed Automata for the Verification of Safety Applications. Verification and validation of safety applications based on PLCopen safety function blocks Verifikation und Validierung sicherheitsgerichteter SPS-Programme. On Formal Verification of Function Block Applications in Safety-related Software Development. Function Block Diagram to UPPAAL Timed Automata Transformation Based on Formal Models Towards an Automated Verification Process for Industrial Safety Applications A methodology to upgrade legacy industrial systems to meet safety regulations Formale Verifikation von Sicherheits-Funktionsbausteinen der PLCopen auf Modell- und Code-Ebene Verification and Validation of Safety Applications based on PLCopen Safety Function Blocks using Timed Automata in Uppaal Control of a Forced-Circulation Evaporator System as a Case Study for Control Engineering Education