Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks (2011)


Kindermann Roland , Junttila Tommi , Niemelä Ilkka

  • PAGES:
  • 185-194


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