Applying model checking to analysing safety instrumented systems

摘要

There is an ongoing change in the industry in which old analogue instrumentation and control (I&C) systems are replaced with new digital ones. New digital systems enable more complex control tasks and especially their application to safety instrumented systems (SIS) has created a need for new verification methods such as model checking.Our goal is to study the applicability of model checking methods to a real safety instrumented system used in industry and to evaluate whether such a system can be modelled on a level which, on one hand, enables verification of relevant safety properties and, on the other hand, keeps the size of the model feasible. A central objective is also to create a general methodology for applying model checking to analysing safety instrumented systems.As a case study we modelled an application of UTU Falcon arc protection system along with its environment with NuSMV modelling language. Moreover, we used NuSMV to verify this model against the most relevant safety properties for the system.Our results indicate that model checking seems to be a promising method for verification of safety instrumented systems.