Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks

Safety instrumented systems (SIS) monitor industrial processes and automatically react on dangerous situations. SIS often consist of both logical and time-dependent building blocks. This paper introduces symbolic timed transition systems, a formalism designed for concise and modular description of SIS with clocks and similar time-dependent systems. Furthermore, an implementation of symbolic timed transition systems as an extension to NuSMV is devised. Two ways of checking properties on symbolic timed transition systems are developed: complete, region-abstraction-based model checking using binary decision diagrams and SMT-based bounded model checking. Both approaches are evaluated experimentally.