Applying model checking to analysing safety instrumented systems

No Thumbnail Available
Journal Title
Journal ISSN
Volume Title
Faculty of Information and Natural Sciences | D4 Julkaistu kehittämis- tai tutkimusraportti taikka -selvitys
Degree programme
ix, 62
TKK reports in information and computer science, 5
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.
model checking, safety instrumented systems
Other note
Permanent link to this item