Unified Functional Safety Assessment of Industrial Automation Systems

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.La norme IEC 61499 apporte une méthode de conception basée sur les modèles pour construire des systèmes d'automatisation industriels complexes. Cependant, le ux de conception existant ne permet pas de traiter de façon adéquate la question importante de la sûreté fonctionnelle. Jusqu'à présent, l'analyse de la sûreté fonctionnelle était traitée en dehors du ux de conception, par les normes telles que IEC 61508, qui fournissent des lignes directrices pour l'évaluation de la sûreté en utilisant des techniques quantitatives et qualitatives. Dans cet article, nous proposons une approche globale et uni ante pour e ectuer l'évaluation de la sûreté fonctionnelle quantitative et qualitative de systèmes IEC 61499, telle que prescrite par la norme IEC 61508. L'approche proposée utilise la véri cation probabiliste pour l'analyse uni ée des aspects tant qualitatifs que quantitatifs des systèmes. Notre approche convertit des systèmes IEC 61499 dans un langage accepté par le model-checker PRISM. Cette traduction est sûre et préserve la sémantique d'exécution du système d'origine, et permet d'utiliser PRISM pour e ectuer l'évaluation de la sûreté fonctionnelle des systèmes IEC 61499. Nous utilisons notre approche pour analyser un exemple tiré du monde réel, et nous montrons que notre technique est adaptée pour l'analyse qualitative et quantitative