The IEC 61499 standard allows a model-based esign approach to build complex industrial automation systems. However, the existing design ow does not adequately address the key issue of functional safety. Functional safety analysis is covered externally to the design ow by safety standards like IEC 61508, which provide guidelines for the purpose of safety assessment using quantitative and qualitative safety analysis techniques. In this paper, we propose a comprehensive and unifying approach for performing IEC 61508-prescribed quantitative and qualitative functional safety assessment of IEC 61499 systems. The proposed approach employs probabilistic veri cation for the uni ed analysis of the qualitative and the quantitative aspects of the system. Our approach converts IEC 61499 designs into language accepted by the Prism probabilistic model checker. This conversion is sound and preserves the execution semantics of the original system, and enables techniques for assessing the functional safety of IEC 61499 designs using the Prism model checker. We use our approach to analyse a realworld example, and show that our technique is suitable for combined qualitative and quantitative analysis.
