Applying Model Checking to Analysing Safety Instrumented Systems

Reference:

Matti Koskimies. Applying model checking to analysing safety instrumented systems. Research Report TKK-ICS-R5, Helsinki University of Technology, Department of Information and Computer Science, Espoo, Finland, June 2008.

Abstract:

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 it's 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.

Keywords:

Model checking, safety instrumented systems

Suggested BibTeX entry:

@techreport{TKK-ICS-R5,
    address = {Espoo, Finland},
    author = {Matti Koskimies},
    institution = {Helsinki University of Technology, Department of Information and Computer Science},
    month = {June},
    number = {TKK-ICS-R5},
    pages = {x+62},
    title = {Applying Model Checking to Analysing Safety Instrumented Systems},
    type = {Research Report},
    year = {2008},
}