A comparison of model checking techniques for cause and effect matrix based controller logic of safety instrumented systems

Abstract

Safety Instrumented Systems (SIS) are safety critical mechanisms that seek to reduce the probability of dangerous events within industrial plants. The behavior of said systems consists of measuring a process’ state via a sensor, making a decision based on a pre- established control logic and activating actuators such that the process is guided back to a safe state in case an undesirable situation is encountered. During the controller’s development phases, errors might be accidentally introduced, causing the behavior of the implemented logic to be incoherent with the one specified. Thus, methods to verify the controller software logic must be applied within the development methodology. Model Checking is a method that uses mathematical modeling to computationally search for errors within a system. In this project, methods for model generation from Ladder diagrams and property extraction from a Cause & Effect Matrix specification are outlined. Then, two Symbolic Model Checking methods, Binary Decision Diagrams (BDD) and Satisfiability Modulo Theory (SMT), have their accuracy and efficiency evaluated in the context of SIS logic with temporal requirements. It was found that while SMT based methods have difficulty with systems in which the timed logic is complex, BDD based methods were effective in determining the existence or absence of errors.

Sistemas Instrumentados de Segurança (SIS) são mecanismos críticos que visam diminuir a probabilidade de eventos perigosos em plantas industriais. O princípio de funcionamento de tais sistemas consiste em medir o estado de um processo através de sensores, tomar uma decisão com base em uma lógica de controle pré-estabelecida e acionar atuadores de forma a guiar o processo a um estado seguro caso necessário. Durante as etapas de desenvolvimento do controlador, erros podem ser acidentalmente introduzidos, de modo que o comportamento do sistema seja incoerente com o especificado. Portanto, meios de verificação da lógica implementada devem ser aplicados na metodologia de desenvolvimento. Model Checking é um método que utiliza modelagem matemática para procurar computacionalmente erros dentro de um sistema. Neste projeto, métodos para geração de modelos a partir de diagramas Ladder e extração de propriedades de matrizes Causa e Efeito são delineadas. Em seguida, dois métodos simbólicos de Model Checking , Diagramas de Decisão Binária (BDD) e Teoria de Módulo de Satisfatibilidade (SMT), tem sua eficiência e acurácia avaliadas dentro do contexto de lógica de SIS com requisitos temporais. Foi encontrado que enquanto métodos SMT tem dificuldade com sistemas nos quais a lógica temporal é complexa, métodos BDD foram efetivos em determinar a presença ou ausência de erros.