Model-Based Analysis of a Stepwise Shutdown Logic
Kim Björkman, Juho Frits, Janne Valkonen, Keijo Heljanko, Ilkka Niemelä · 2009
Modern digitalized Instrumentation & Control (I&C) systems set new challenges for safety evaluation. Model checking is a promising formal method that can be used for verifying the correctness of system designs. A number of efficient model checking systems are available offering analysis tools that are able to determine automatically whether a given state machine model satisfies the desired safety properties. Model checking can also handle delays and other time-related operations, which are crucial in safety I&C systems and are challenging to design and verify. Two types of model checking approaches are studied to verify safety logic designs involving timing aspects. The first approach uses timed automata as the modelling framework and the other employs finite state machines typically used in verifying hardware. The approaches are compared using two similar designs of a safety logic demonstrating how small changes in the design can lead to unexpected errors that are hard to detect without using model checking techniques. A straightforward approach to modelling such designs using timed automata and finite state machines